A GitHub Repo Claims a Lean Proof That Walter Trump's 1979 Packing of 11 Squares Is Optimal, Checked Across 7,920 Modules

A GitHub repository published this week claims a complete, machine-checked proof that the best known way to pack 11 unit squares into a larger square cannot be beaten. The repository, 11SquaresFormalized, reports that a verification run accepted all 7,920 Lean modules with zero admissions.

The packing in question needs a container with a side of about 3.87708359 unit squares. Walter Trump found it in 1979, according to a catalogue of squares-in-squares records maintained by David Ellsworth. That page marks the arrangement as rigid but does not list it as proven optimal.

What the 11-square proof claims

The repository gives the optimal side length as T = (6u+4)/(1+2u-u^2), where u is the unique root between 9/25 and 37/100 of a degree-8 polynomial. It evaluates to about 3.8770835900228141773. Squares may sit at any angle, may touch the boundary, and must have disjoint interiors.

The proof is written in Lean 4 version 4.34.1 against a pinned revision of Mathlib, the community maths library. The repository credits EvolvingPrograms, a GitHub user named @ctjlewis and project contributors for the formalisation and the verification run. The run is documented in a report dated 2026-10-06 in the file name.

Where 11 squares sat among the solved cases

Ellsworth's catalogue lists optimality proofs for only some counts of squares. Eleven was not one of them.

Squares (n)	Side length	Status on Ellsworth's page
10	3 + ½√2	Proved by Walter Stromquist, 2003
11	about 3.87708359	Found by Walter Trump, 1979; no proof listed
13	4	Proved by Wolfram Bentz, August 2009

Other counts on the page, including 83 and 87, are also unproven. Hacker News commenter sheept said that those packings may therefore still be improvable.

The repository is silent on whether AI wrote it

The Hacker News submission, posted by bluepeter, titled the work "AI-assisted proof of optimal packing for 11 squares". The repository itself names no model or tool and does not say AI was involved. Commenter fwip said the README "appears to be entirely LLM-written". That is an observation about the prose, not about the proof.

The readme contains no diagram of the packing, a gap commenters agnishom and meowkit both raised. It links no paper and mentions no prior record.

Commenter DevelopingElk described the method as a computer-assisted search over an unavoidable set of configurations, and argued that AI lowers the effort needed to formalise such proofs. That fits a pattern the site has reported before, when Erdős Problems froze proof submissions after a flood of machine-assisted claims.

What the Lean check does and does not cover

The repository carries a plain caveat. Selected numerical certificate checks use Lean's native_decide, so the final theorem trusts Lean's kernel and its native compiler, not the kernel alone. The README says this is not a kernel-only verification claim.

It adds that reaching 100% of compiled modules is not enough by itself. The final output must also read OPTIMALITY_PROVED_WITH_NATIVE_CERTIFICATES, with zero admissions. The run used a larger runner supplied by EvolvingPrograms, and the page does not give a cold-build time for anyone reproducing it.

That makes it a checkable claim. Anyone with the pinned toolchain can run scripts/run_verification.sh from the repository. Another recent case of AI-linked technical work is DIVD's report of an AI agent chaining two Zammad zero-days, though that one was judged by researchers rather than a proof checker.

No mathematician has publicly confirmed the result, and no journal or preprint server entry is linked from the repository. Whether Ellsworth's catalogue will move the entry for n = 11 from found to proved is not addressed on his page.