Walter Trump's 1979 packing of 11 unit squares proved optimal, with a full Lean verification (AI involvement reported, unconfirmed)
On Oct 6, 2026 the GitHub project 11SquaresFormalized reported a complete Lean 4 verification (7,920 modules, zero admissions) that Walter Trump's 1979 packing of eleven unit squares in a square is optimal, with side s(11) ≈ 3.87708359. It formalizes a computer-assisted certificate proof posted on Sept 29. Startup Fortune reported that OpenAI's Astra and Anthropic's Claude were credited as contributors, but the repositories' acknowledgements reviewed here do not mention AI models.
Key facts
- Result: the minimum side of a square holding 11 unit squares is T = (6u+4)/(1+2u−u²) ≈ 3.8770835900228, where u is the root in (9/25, 37/100) of 5u⁸−10u⁷−2u⁶+14u⁵+12u⁴−6u³+2u²+2u−1 = 0; rotations and boundary contact allowed
- Underlying proof (repo 11SquaresOptimal, Sept 29, 2026, by GitHub user Queuingtheorydotcom): a center cover reduces any smaller packing to 2,184 cell patterns; exact certificates exclude 2,180; symmetry reduces the last four to one case, which is closed by a branch cover and an isolation argument. The README says it is 'not a completed Lean/formal proof' and not peer-reviewed
- Formalization (11SquaresFormalized, verification report dated 2026-10-06): 7,920 Lean modules accepted, 0 sorry/admissions, 2,234 audited theorem targets, status OPTIMALITY_PROVED_WITH_NATIVE_CERTIFICATES; Lean 4.34.1 + pinned Mathlib
- Trust model: numerical certificates use native_decide, so the theorem trusts Lean's kernel and native compiler, 'not a kernel-only verification claim'
- Credits in the repo: EvolvingPrograms and @ctjlewis (verification runner), @wand125 (n11-optimality-lean formalization), Benjamin Gurevitch, @Julian-JJ, @Guzhou0806, Queuingtheorydotcom (the proof); Walter Trump for the packing
- AI role: Startup Fortune (Oct 7) says the work credits 'OpenAI's Astra and Anthropic's Claude' as direct contributors. The README, ACKNOWLEDGEMENTS and PROVENANCE files and recent commit messages checked on 2026-10-07 do not mention AI models. Treat the AI claim as unverified
- History: Trump found the tilted arrangement in 1979; the problem was popularized by Martin Gardner and Erich Friedman's 'Squares in Squares' pages, and became an internet meme through xkcd #2740 ('Square Packing', 2023)
Science result
- Field
- mathematics / discrete geometry (square packing)
- Problem
- Optimality of Walter Trump's 1979 packing of 11 unit squares in a square (s(11)) (open since 1979)
- Result
- Proof that s(11) = T ≈ 3.87708359 (Trump's packing is optimal), via a computer-assisted certificate proof formalized in Lean 4 with native_decide numerical certificates
- Human role
- Human-led open-source project; AI involvement (Astra, Claude) reported by Startup Fortune but not stated in the repositories
- Verification
- Lean 4 formalization, 7,920 modules, zero admissions; trusts Lean kernel and native compiler; not peer-reviewed
- Status
- pending
What happened
How tightly can eleven unit squares be packed into a square? Walter Trump's 1979 answer uses a tilted cluster and had never been proved
best. On Sept 29, 2026 a GitHub user posted a computer-assisted certificate proof. Within a week, several contributors turned it into a full
Lean 4 development, which passed a complete verification run on Oct 6. The proof relies on many numerical certificates checked with
native_decide, so it trusts Lean's compiled code as well as its kernel.
Why it matters
It settles a well-known open case in packing theory, widely known from xkcd. If the reported AI credit is confirmed, it would be an example of models from two rival labs helping to formalize a decades-old result. That needs a primary source (an X post or the contributors' own statement) before it can be relied on.
Changelog
- 2026-10-07: created (sweep 2026-10-07, Google News: Startup Fortune); AI credit not found in repo files
People
Related events
- Math Inc's Gauss formalises Viazovska's sphere-packing proofs in dimensions 8 and 24, fixing errors in the originals ★★★★
- Summer 2026 flood: dozens of named conjectures settled on arXiv with disclosed AI help (July–September catalogue) ★★★★
Sources (6)
- codeGitHub: Queuingtheorydotcom/11SquaresFormalized (Lean formalization)
- codeVerification report 2026-10-06
- codeGitHub: Queuingtheorydotcom/11SquaresOptimal (computer-assisted proof, Sept 29)
- codeGitHub: wand125/n11-optimality-lean
- pressStartup Fortune: AI models formally proved Walter Trump's 1979 square packing is optimal
- docsErich Friedman: Squares in Squares
id: 2026-10-06-eleven-square-packing-optimality-lean · updated 2026-10-07 · open in the interactive timeline