Eleven Squares, Checked by Computer: A 7,920-Part Proof Passes

A computer-checked proof for the best packing of 11 equal squares has passed verification with fast numerical checks, according to the 11SquaresFormalized repository. The statement was published on 2026-10-07 GMT and is listed as the repository's current authoritative result.

The verification run, named EvolvingPrograms, accepted all 7,920 local Lean modules. Lean is the proof-checking language, and modules are its separately checked files. The final audit reports zero admissions, meaning no gaps left as unchecked placeholders.

The broader context for that scale is a highly split-up project. A count of 7,920 points to thousands of small units rather than one long proof script, with checking spread across them.

The claimed best size is given as an exact formula: T = (6u+4)/(1+2u-u^2), where u is the single root in the interval (9/25, 37/100) of 5u^8-10u^7-2u^6+14u^5+12u^4-6u^3+2u^2+2u-1=0. 11SquaresFormalized repository That pairing gives a checker both the value and narrow bounds to locate it. The matching layout has side length about 3.8770835900228141773. The rules allow squares to rotate and to touch each other or the outer border, but their interiors cannot overlap.

Reproducibility is fixed to specific versions. The repository pulls proof sources and build settings from commit 1bf942a7af1ea330e95489d8997deebd4227ca71, and it pins Lean 4.34.1 and Mathlib revision d13f23b723b8a846827a245b89c10fc7d3f11612, the shared math library. 11SquaresFormalized repository

The practical context here is version drift. Lean and Mathlib change fast, and without those pins a formalization can stop building within months.

The README describes how upstream certificate results are combined with local work, listing ElevenSquare/Tasks/, geometric arguments, checkers, certificate data, and local analytic proofs. The public repository is hosted under the GitHub account Queuingtheorydotcom and is described as a Lean formalization of the optimality proof for 11-square packing.

The trust statement is narrow. The final theorem relies on Lean's kernel, the small core that checks logic, plus the native compiler that runs fast code, and it is not claimed as kernel-only verification. The native numerical certificates speed up checking, but they put that native code path inside the trusted base along with the kernel.

The broader context here is the trade-off in large computer-checked proofs between completeness, auditability, and speed. Zero admissions means the audit found no placeholder gaps in the final checked files. It does not remove the need for trust, which stays concentrated in the kernel, the toolchain, and the native code used for the certificates.

In my view, the most useful detail for people who build such proofs is the combination of exact formula, isolating interval, pinned toolchain, and source commit. The formula removes ambiguity about the claimed size. The interval makes the root findable by computation. The pinned Lean and Mathlib versions make the build repeatable. The source commit identifies the exact input that was checked.

Looking at what this enables, the pattern can be reused beyond packing puzzles. Branching geometric cases too heavy to check step by step inside the kernel can be cleared with fast native certificates, while the surrounding combinatorial and analytic reasoning stays in Lean.

Worth flagging is the maintenance cost. A 7,920-module collection tied to a fixed toolchain snapshot checks cleanly now, but keeping it checkable as Lean and Mathlib change will take ongoing updates or a preserved container with the pinned setup. That is normal for work at this scale, and listing the pins up front makes the preservation job concrete.