From Newsgroup: sci.logic

Hi,

How about this constraint solving problem:

"For 4|u4 magic squares, itrCOs unknown whether a
magic square of squares exists. This is the most
famous open case. No one has found one, and no
proof exists that one cannot exist." https://en.wikipedia.org/wiki/Magic_square_of_squares

Well the 4x4 problem fits well, I am currently
working on a CLP(FD) that can detect quadratic forms.
Something to explore as part of the Railgun CLP(FD)

project. Just joking. I saw the explosion of a
4x4 magic square today, by mistake I changed L ins
1..4 into L ins 1..9, and boom, no more solutions

obtainable in short time.

Bye

Mild Shock schrieb:

Hi,

This is a brief description of a project that
has already autoformalized a large portion of
the general topology from the Munkres textbook
(which has in total 241 pages in 7 chapters
and 39 sections).

The proof checker is Chad Brown's higher-order
set theory system Megalodon, and the core library
is Brown's formalization of basic set theory
and surreal numbers (including reals, etc).
The rest is some prompt engineering and
technical choices which we describe here.

130k Lines of Formal Topology in Two Weeks
https://arxiv.org/abs/2601.03298

Is this the end to the mess, of the same
theorem proved with proof assistant A, but
using set theory, and also proved with proof
assistant B, but using type theory.

How malleable are LLM generated proofs?

Bye

Mild Shock schrieb:

Hi,

Good Morning Vietnam, the HPC-AI Convergence
doesn't sleep. Here a friendly reminder of
the Sudoku leader board (Topn87 Challenge):

#1: jczsolve / Rust WASM
-a-a-a-a Solving 87 Sudokus in 0.006 seconds (0 sec / Sudoku)
-a-a-a-a https://emerentius.github.io/sudoku_web/

#2: Kudoku / JavaScript
-a-a-a-a Solving 87 Sudokus in 0.043 seconds (0.0004 sec / Sudoku)
-a-a-a-a https://attractivechaos.github.io/plb/kudoku.html

#3: Picat / import cp. solve([ff],L)
-a-a-a-a CPU time 0.175 seconds
-a-a-a-a https://picat-lang.org/

#4: Picat / import sat. solve(L)
-a-a-a-a CPU time 0.373 seconds
-a-a-a-a https://fmv.jku.at/kissat/

Tested on Windows 11, with a AMD Ryzen AI 350

Didn't test yet GNU Prolog, ECLiPSe Prolog or
Ciao Prolog. So whats next? Well beat #1 by
tapping into an NPU of Copilot+ PC.

Have Fun!

Its Winner Winner Chicken Dinner time again...

Bye

--- Synchronet 3.21a-Linux NewsLink 1.2