Astra and Claude are credited on a Lean proof that Trump's 1979 packing of eleven squares is optimal

Forty-seven years ago, Walter Trump arranged eleven unit squares inside a larger square at a tilt of roughly 40.182 degrees and got a side length of about 3.87708, tighter than any grid-aligned layout. Mathematicians believed it was optimal. Nobody had proved it. On October 6, a GitHub user going by Queuingtheorydotcom, real handle ManassehA06, published a complete Lean formalization showing that any other packing of eleven unit squares reduces to Trump's, up to flip, rotation or relabeling. The announcement credits OpenAI's Astra and Anthropic's Claude, alongside named human collaborators, as direct contributors.

What the proof actually settles

Square packing is a deceptively simple game: how small a square can you draw around n smaller unit squares without any overlap. For most small n the answer is the obvious one, axis-aligned rows inside an integer-sided box. Eleven is the first case where that pattern breaks. Trump's 1979 arrangement tilts a central cluster so the pieces interlock, gaining a sliver of space a rigid grid cannot match. For decades it stood as the best known packing rather than a proved optimum, because nobody had ruled out some stranger, still-tighter configuration.

The formalization closes that gap. The repository, called 11SquaresFormalized, states s(11) = T, where T is roughly 3.87708359002281, defined as the root of a degree-eight polynomial. It proves two things: no packing of eleven unit squares fits in a square of side shorter than T, and the only packings that achieve T are Trump's up to symmetry. The Wikipedia page on square packing now lists n = 11 as resolved and records the value as approximately 3.877084, ending a 47-year gap in the table.

Why a Lean proof is a different kind of claim

Headlines about AI solving math deserve a specific kind of suspicion, and this one has a clean answer. Lean is a formal proof language: a proof written in it is checked by a computer kernel that verifies every logical step follows from the last. A persuasive English argument can hide a gap that survives years of casual reading. A Lean proof that compiles cannot hide one, because the kernel refuses a step that does not follow. The distinction is between a claim and a certificate.

The repository leans on that standard. Its verification report says a clean run accepted all 7,920 local Lean modules with zero admissions, Lean's term for an unproved obligation, and the build pins Lean 4.34.1 and a fixed Mathlib revision so the check can be reproduced. The same discipline runs through the formalization that predates it, such as Vals AI's ten-agent Thomson problem proof, which also shipped its own verification trail.

Check	What it establishes
Full Lean build	every step type-checks, no admissions
Axiom query	only Lean's standard axioms are used
Independent registry review	the statement matched an outside framework

One honest wrinkle is recorded in the README rather than buried: the most expensive numerical certificate checks use Lean's native_decide, which trusts the compiler for those computations, while the geometry, checker soundness and proof assembly keep ordinary kernel-checked proofs. That is a smaller trust surface than "solved by AI," and the repo labels it as such.

The skeptical reading

Two cautions belong next to the credit line. First, an earlier version of this formalization carried six explicit "sorry" markers, Lean's placeholder for a step that is asserted but not proved, before the October 6 version closed them out. The history is public, and it matters: a formalization can look finished while several of its load-bearing steps are still hand-waved. Second, the separate jlevy/squares project, which audits and catalogs square-packing results, pulled the formalization into its registry as result T-060 and a related uniqueness claim as T-112, flagging that the statement was checked against its own framework before acceptance. That is a real independent check of the statement, though not yet of the whole proof.

The human share is the part the headlines compress. Trump found the packing by hand. The named human collaborators, including ojoshe, Kleddamag, wand_125, Guzhou0806 and ctjlewis, wrote most of the surrounding architecture, the definitions, the certificate infrastructure and the glue, that the models' contributions sit inside. What the models added was real. It was not the whole.

The credit line is the story

The more interesting question is why two rival labs' models are named on the same result at all. This is not the first time Astra and Claude have crossed paths on formal mathematics. OpenAI introduced Astra on August 1 with ten solved problems in mathematics and theoretical computer science, each shipped with a Lean 4 certificate, and Anthropic's Levent Alpoge said at the time that Claude, given the same prompts and no internet access, reproduced roughly half of those ten within 24 hours. That symmetry, one lab's model matching much of another's benchmark, is why a joint credit reads less like a collaboration and more like a scoreboard. It follows the pattern of Claude's Fermat's Last Theorem formalization and OpenAI's push to absorb hundreds of proofs into machine-checked form. The informal reception ran along the same lines: the thread in r/singularity drew roughly 650 points, and the discussion there focused as much on the credit split as on the geometry.

What would settle it

Three markers would move this from a compiled artifact to an accepted theorem. Independent refereeing, which no kernel provides: Lean shows the argument is valid given its hypotheses, not that the hypotheses describe what everyone means by packing squares. Upstreaming the result into a maintained library such as Mathlib, where other mathematicians can build on it. And a statement of scope, evidence that the same method reaches the next unresolved case, n = 12, rather than stopping at the one instance where the search space happened to be tractable. Lean verifies the argument here. It says nothing about the interest of the result, and it does not take a side in the race between the labs whose models were credited.