AI-assisted Lean proof verifies optimal packing of 11 squares

A GitHub repository called 11SquaresFormalized has landed a complete Lean formalization of the optimality proof for packing eleven congruent squares into the smallest possible square container. The work reached Hacker News's front page under the headline "AI-assisted proof of optimal packing for 11 squares", and according to the repository, an external verification run accepted all 7,920 local Lean modules with a final audit that reported no admissions — nothing was accepted without being checked.

What the theorem says

The result pins down the minimal side length of a square that can hold eleven smaller squares, under a deliberately permissive model described in the README: squares may sit at arbitrary orientations rather than only axis-aligned, they may make legal contact with the boundary and with each other, and their open interiors must stay disjoint.

The optimal side length is expressed exactly as (6u+4)/(1+2u-u^2), where u is the unique root between 9/25 and 37/100 of the degree-eight polynomial 5u^8 - 10u^7 - 2u^6 + 14u^5 + 12u^4 - 6u^3 + 2u^2 + 2u - 1 = 0. Numerically, the construction that attains the bound measures about 3.8770835900228141773. The headline statements — unconditional optimality and a side-length lower bound — live in ElevenSquare/Optimality.lean, with axiom queries for those public targets in ElevenSquare/Verification.lean.

How the proof is built

The proof spans a layered codebase. ElevenSquare/Foundations.lean contains the geometry, an exact endpoint, the attaining construction, a closed-cell cover, and a reduction to finitely many cases. The Tasks and Sqpack directories hold the geometric arguments, certificate checkers, generated proofs, simplifications and local analytic work, while a directory named Pending preserves the original public interfaces, now discharged by the integrated proof — the name is historical, the README notes.

Everything is pinned for reproducibility. The repository imports its proof sources and build configuration from commit 1bf942a7af1ea330e95489d8997deebd4227ca71, runs on Lean 4.34.1, and fixes the Mathlib revision d13f23b723b8a846827a245b89c10fc7d3f11612.

What you are trusting

The README is unusually explicit about the trust model. Selected expensive, exact numerical certificate checks are discharged using native_decide, so the final theorem depends on Lean's kernel together with the native compiler — and the project states plainly that this is not a kernel-only verification claim. Ordinary Lean proofs still cover the geometry, checker soundness and the assembly of the final theorem, and each approved numerical declaration is recorded with its exact source hash in verification/native-certificates., keeping the enlarged trusted surface small and auditable.

Reproducing the run

Verification is scripted. On Linux, with Python 3, Git, curl and tar available, running scripts/run_verification.sh --bootstrap --jobs 2 prepares the pinned toolchain and compiles everything serially; macOS users must first install the elan launcher. The command checks every local module and then performs a final source, receipt, dependency and axiom audit. A genuine pass requires three conditions together: the OPTIMALITY_PROVED_WITH_NATIVE_CERTIFICATES flag, an audit with nothing admitted, and trust_model: lean_kernel_and_native_compiler in the final result — compiling 100 percent of modules alone is explicitly not sufficient. A lighter option, scripts/check_sources.py, validates the sources without Lean at all.

Two caveats come with the release. The successful source run used EvolvingPrograms' larger runner, so the project does not establish a cold-build runtime or guarantee a two-to-three-hour run on macOS. And the README warns against running historical materialization commands or verify.py --setup on this snapshot, because they would restore superseded generated sources.

Why it matters

Square packing is a classic geometric optimization problem where even small cases can require intricate arguments, and optimality claims have historically been difficult to verify by hand. A machine-checked proof shifts the burden: readers no longer need to trust the authors' algebra, only a small and inspectable toolchain that anyone can re-run from the pinned snapshot.

The project also models honest trust accounting. Rather than overstating its guarantees, it declares exactly which numerical checks fall outside Lean's kernel and publishes the hashes of the declarations involved. That discipline matters more as AI systems take a larger role in assembling formal proofs — the Hacker News framing of this work as AI-assisted, alongside credits to EvolvingPrograms, @ctjlewis and other contributors, sketches a sensible division of labor: machines and AI tooling help build and iterate on a massive proof, while an independent verifier and a reproducible audit supply the actual mathematical guarantee.