A public Lean 4 repository is reporting a complete formalization of the optimality proof for packing eleven unit squares into the smallest possible square, a problem tied to Walter Trump’s 1979 construction. The repository says its full verification run accepted all 7,920 local Lean modules with zero admissions, but independent reviewers still distinguish that project-reported run from a retained third-party rebuild and human expert review.
That distinction matters because this is not simply another claim that an AI model produced a mathematical argument. The public repository, 11SquaresFormalized, contains the Lean source, pinned toolchain, verification scripts and theorem statements. Its central claim is that the optimal side length is approximately 3.8770835900228141773 for eleven unit squares when arbitrary orientations and legal boundary contact are allowed.
The result traces back to a packing found by Walter Trump in 1979. By 2026, that makes the underlying construction 47 years old. What is new is the attempt to encode the complete optimality argument in a proof assistant so that the chain can be checked mechanically rather than accepted only as prose, hand calculation or numerical evidence.
What the Lean repository says it verified
The repository’s README says the complete optimality proof passed verification with native numerical certificates and that an EvolvingPrograms run accepted all 7,920 local modules. It also reports zero admissions, meaning the final proof is not relying on Lean placeholders such as an admitted theorem to skip a missing step.
The public theorem is presented through the ElevenSquare.optimality development. The repository states the exact optimal side through an algebraic expression and gives the numerical value as about 3.8770835900228141773. The geometric model allows independently rotated unit squares, contact with the boundary and disjoint open interiors.
For readers outside formal mathematics, the important point is that Lean is checking a precisely encoded theorem against a precisely encoded proof. That is much stronger than asking a language model whether an informal argument “looks right.” But it is still only as meaningful as the formal statement, definitions and trusted computing base that have been encoded correctly.
Why the trust model matters
The repository is unusually explicit about its trust boundary. Selected expensive numerical certificate checks use Lean’s native_decide, so the project says the final theorem trusts both Lean’s kernel and the native compiler. It specifically says this is not a kernel-only verification claim.
That does not make the proof invalid. It means the verification claim should be described accurately. In formal methods, a small trusted kernel is attractive because fewer software components must be assumed correct. When native execution is used to discharge large computations, the trusted base expands to include the compiler path used for those computations.
The repository provides a verification command intended to replay the project and says a successful run should end with the marker OPTIMALITY_PROVED_WITH_NATIVE_CERTIFICATES, zero admissions and the declared trust model. It also warns that compiling every module is not enough without the final source, receipt, dependency and axiom audits.
AI helped assemble the formalization, but Lean is the verifier
The independent Squares Project case record reports that the formalization’s author credited Astra and Claude with helping formalize the optimality result in Lean. That is important context for AI-assisted mathematics, but it does not mean either model should be described as having independently proved the theorem.
A more accurate description is that AI systems helped produce or assemble formal proof code, while Lean checks whether the formal derivations establish the encoded theorem under the project’s definitions and trust assumptions. Human judgment still matters at another layer: whether the formal statement faithfully represents the intended mathematical claim.
This division of labor is becoming increasingly important in AI-assisted research. Language models can accelerate translation, tactic search and proof construction, while proof assistants can reject invalid formal steps. The combination is far more auditable than relying on model confidence alone, but it does not eliminate the need to review definitions, theorem statements and assumptions.
The remaining independent-review gap
The Squares Project treats the new formalization as significant evidence, but its own case record is careful about what it has independently established. It says the source’s full verification run is recorded as reported and that the record does not yet rest on a complete retained third-party build. It also says no independent human expert review of the full formalization is retained there yet.
That caveat prevents the strongest possible formulation of the story. It would be premature to say that the 47-year-old problem has now been universally settled solely because an AI-assisted Lean repository exists. A better description is that the project has published a complete formalization and reports a successful large-scale verification run, while independent reproduction and expert review are still catching up.
For AI research, that is arguably the more interesting development anyway. The important shift is not that a chatbot produced another mathematical manuscript. It is that AI-assisted mathematical work is increasingly being pushed into environments where proof obligations can be inspected, rerun and challenged at the code level. If independent builders reproduce the full 11SquaresFormalized run and experts sign off on the statement fidelity and trust model, this case could become a strong example of how AI-generated mathematical work moves from plausible argument to auditable formal evidence.
