From Newsgroup: sci.logic

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

--- Synchronet 3.21b-Linux NewsLink 1.2