AI-assisted proof of optimal packing for 11 squares
On October 6, a GitHub user going by Queuingtheorydotcom, real handle ManassehA06, published a complete Lean formalization proving that s(11) = T. T is about 3.8771, the side length of Walter Trump's 1979 arrangement, which tilts a cluster of squares in the middle at an angle of about 40.182 degrees. The announcement credits Astra and Claude along with five human collaborators. The repo is approximately 400k lines of lean. There is one caveat. The theorem depends on 13,308 native_decide axioms, so it trusts Lean's compiler as well as its kernel. The full verification ran in a private repository. Joshua Levy's Squares Project, which tracks this work, says no complete build this record can rest on, and no human expert's review of the formalization, is retained yet. The team has started working on a human readable and human written paper. For AI founders, this shows frontier models producing machine-checkable research at a scale no human reviewer could read line by line. The remaining question is verification infrastructure: compiler trust, reproducible builds and independent audits. Startups such as Axiom Math are already building products around that gap.
