Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.prolog > #15227

Chad Brown's Megalodon goes LLM (Was: Good Morning, Vietnam! Sudoku 2026 Challenge)

Show all headers | View raw

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
> 

Back to comp.lang.prolog | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

Good Morning, Vietnam! Sudoku 2026 Challenge Mild Shock <janburse@fastmail.fm> - 2026-01-05 12:11 +0100
  Help! An AI found a Heuristic for me (Was: Good Morning, Vietnam! Sudoku 2026 Challenge) Mild Shock <janburse@fastmail.fm> - 2026-01-10 02:38 +0100
    Failed coping with AI: Moshe Vardi (Was: Help! An AI found a Heuristic for me) Mild Shock <janburse@fastmail.fm> - 2026-01-10 03:02 +0100
      A new proposal: The Gladiator Test (Was: Failed coping with AI: Moshe Vardi) Mild Shock <janburse@fastmail.fm> - 2026-01-10 03:20 +0100
  Chad Brown's Megalodon goes LLM (Was: Good Morning, Vietnam! Sudoku 2026 Challenge) Mild Shock <janburse@fastmail.fm> - 2026-01-10 17:19 +0100
    Magic square of squares [Richard Guy] (Re: Chad Brown's Megalodon goes LLM) Mild Shock <janburse@fastmail.fm> - 2026-01-22 01:40 +0100

csiph-web