Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > sci.physics > #894958
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Newsgroups | sci.physics |
| Subject | Magic square of squares [Richard Guy] (Re: Chad Brown's Megalodon goes LLM) |
| Date | 2026-01-22 01:48 +0100 |
| Message-ID | <10krs43$ffk2$1@solani.org> (permalink) |
| References | <10jg6fe$2nfdv$5@solani.org> <10jtub5$30eb8$4@solani.org> |
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 >
Back to sci.physics | Previous | Next | Find similar | Unroll thread
Magic square of squares [Richard Guy] (Re: Chad Brown's Megalodon goes LLM) Mild Shock <janburse@fastmail.fm> - 2026-01-22 01:48 +0100
csiph-web