From: janburse@fastmail.fm   
      
   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)