Astra and Claude Credited on Lean Proof of 11-Square Packing

A GitHub repository called 11SquaresFormalized went up on October 6, with all 7,920 of its local Lean modules verifying and zero admissions in the final audit. The claim: that the arrangement of eleven unit squares inside a larger square that Walter Trump found in 1979, side length roughly 3.87708359002281, really is the smallest one possible.

The repository names two AI systems, OpenAI's Astra and Anthropic's Claude, as direct contributors alongside human collaborators including ojoshe, Kleddamag, wand_125, Guzhou0806 and ctjlewis. Earlier versions carried six 'sorry' markers, Lean's placeholder for an unproven step. The October 6 version has none.

As Startup Fortune put it, 'A Lean proof that compiles cannot [hide gaps], because the software simply refuses to accept a step that doesn't follow.' That is a stronger standard than a chat transcript or a written-out argument.

Trump's trick, 47 years ago, was to tilt a cluster of squares at roughly 40.182 degrees instead of aligning them to a grid. What had been missing was a mechanical proof that no tighter arrangement existed. The GitHub README states the complete optimality proof passed verification with native numerical certificates, with the caveat that this is not a kernel-only verification claim.