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

From	Mild Shock <janburse@fastmail.fm>
Newsgroups	comp.lang.prolog
Subject	Magic square of squares [Richard Guy] (Re: Chad Brown's Megalodon goes LLM)
Date	2026-01-22 01:40 +0100
Message-ID	<10krrll$ffat$1@solani.org> (permalink)
References	<10jg69u$2nfdv$1@solani.org> <10jtu6a$30eb8$1@solani.org>

Show all headers | View raw

Hi,

How about this constraint solving problem:

"For 4×4 magic squares, it’s unknown whether a
magic square of squares exists. This is the most
famous open case. No one has found one, and no
proof exists that one cannot exist."
https://en.wikipedia.org/wiki/Magic_square_of_squares

Well the 4x4 problem fits well, I am currently
working on a CLP(FD) that can detect quadratic forms.
Something to explore as part of the Railgun CLP(FD)

project. Just joking. I saw the explosion of a
4x4 magic square today, by mistake I changed L ins
1..4 into L ins 1..9, and boom, no more solutions

obtainable in short time.

Bye

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 comp.lang.prolog | Previous | Next — Previous 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