From: janburse@fastmail.fm   
      
   Hi,   
      
   How about this constraint solving problem:   
      
   "For 4×4 magic squares, it’s 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   
   >>      Solving 87 Sudokus in 0.006 seconds (0 sec / Sudoku)   
   >>      https://emerentius.github.io/sudoku_web/   
   >>   
   >> #2: Kudoku / JavaScript   
   >>      Solving 87 Sudokus in 0.043 seconds (0.0004 sec / Sudoku)   
   >>      https://attractivechaos.github.io/plb/kudoku.html   
   >>   
   >> #3: Picat / import cp. solve([ff],L)   
   >>      CPU time 0.175 seconds   
   >>      https://picat-lang.org/   
   >>   
   >> #4: Picat / import sat. solve(L)   
   >>      CPU time 0.373 seconds   
   >>      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   
   >   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)