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

Groups > sci.physics > #894958 > unrolled thread

Magic square of squares [Richard Guy] (Re: Chad Brown's Megalodon goes LLM)

Back to article view | Back to sci.physics

This discussion starts older than the indexed window; earlier articles aren't shown. The article labeled Started by below is the oldest one visible, not the original post.

Contents

  Magic square of squares [Richard Guy] (Re: Chad Brown's Megalodon goes LLM) Mild Shock <janburse@fastmail.fm> - 2026-01-22 01:48 +0100

#894958 — Magic square of squares [Richard Guy] (Re: Chad Brown's Megalodon goes LLM)

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
> 

[toc] | [standalone]

Back to top | Article view | sci.physics

csiph-web