Eleven squares, a 47-year-old packing problem, and what AI-assisted mathematics is starting to look like when the hype is stripped away.
A Reddit post caught my attention today with the sort of headline that now reliably activates both halves of my brain at once:
Astra and Claude prove a 47-year-old unsolved math problem.
One half goes, wait, seriously?
The other immediately starts looking for the asterisk.
There is an asterisk.
There are several, actually.
But after digging into what happened, I think the less sensational version is more interesting than the headline.
First, the stupid squares
The problem is wonderfully simple to explain.
Take eleven identical unit squares. Put them inside a larger square. You can rotate the little squares however you want, but they cannot overlap.
How small can the outer square be?
That number is usually written as s(11).
In 1979, Walter Trump found an extraordinarily compact arrangement that fits the eleven squares inside a larger square with side length approximately:
3.877083590022814…
And it looks wrong.
Several of the squares are tilted at irritating angles. There are little gaps. Parts of the arrangement look inefficient in the way a badly packed suitcase looks inefficient.
Your visual cortex wants to grab the pieces and straighten them.
But area is not what is being optimized.
The question is not whether there is unused space. The question is whether the walls of the containing square can be pushed any closer together without causing two of the unit squares to overlap.
Trump had shown that 3.877083590… was achievable.
What nobody had managed to prove was that something even slightly smaller was impossible.
That distinction matters enormously.
Finding a good solution gives you an upper bound.
Proving nobody can ever do better gives you the matching lower bound.
Until those meet, you do not know the answer.
For almost half a century, they did not meet.
On September 29, 2026, a computer-assisted proof published by Queuingtheorydotcom closed that gap. The resulting value matches Trump’s construction exactly. The Squares Project now records Trump’s packing as globally optimal.
So the discovery here is not the bizarre tilted arrangement.
That has been sitting around since 1979.
The discovery is the proof that there is nowhere else to look.
This is where the AI part gets interesting
If you stop at the headline, you can easily picture somebody opening two chat windows, typing:
Solve this 47-year-old geometry problem.
and Claude and Astra disappearing into the mathematical wilderness before returning with a theorem.
That is not what happened.
The actual story is much messier, more collaborative, and much closer to what I suspect serious AI-assisted research will increasingly look like.
There were humans directing the work. There was existing mathematics. There were previous lower bounds, computational searches, exact geometric calculations, independent verification work and a growing body of machinery around the packing problem.
GPT-6 Astra was used inside that research process for mathematical reasoning and review. The Squares Project contains Astra-authored structural analysis and explicitly identifies Astra-assisted work in the chain leading to the proof. One such structural review is available in the project repository.
The final global argument did not simply stare harder at the picture.
It reduced a continuous geometric problem, one involving effectively limitless possible positions and rotations, into a finite collection of cases that could actually be attacked.
The proof considers 2,184 structural patterns. It eliminates 2,180 of them, leaving four symmetry-related survivors, then reduces those to the known Trump configuration through additional exact analysis. The project documents that reduction in its N=11 case record.
That is the part I find fascinating.
The problem did not become easy.
The search space became structured.
And frontier AI systems were participating in the process of finding, analyzing and checking that structure.
Then Claude enters the story
The result itself was followed by another step: formalization.
On October 6, the proof’s authors reported a Lean 4 formalization of the complete optimality claim, assembled with assistance from Astra, Claude and human collaborators. The central theorem, ElevenSquare.optimality, states the same global result recorded by the Squares Project. The formalization details are recorded there as well.
Lean is not another chatbot.
It is a proof assistant.
You do not persuade Lean that a proof sounds reasonable. You define your mathematical objects and then provide a chain of deductions that satisfies its formal rules.
That makes this particular AI story more interesting than the familiar pattern of:
LLM generates plausible answer → human squints at it → everybody hopes for the best.
Here, parts of the work can be reduced to artifacts that machines can mechanically verify.
That does not remove the need for trust entirely, though.
And this is where I think reporting on AI mathematics needs to grow up very quickly.
“Formally verified” still has footnotes
The current Squares Project record is unusually transparent about the limitations.
The source reports a complete Lean run containing 7,920 modules with no admitted goals. But portions of the numerical verification use Lean’s native_decide, meaning those computations trust Lean’s compiler in addition to the much smaller logical kernel.
The reported theorem depends on 13,308 native certificate checks.
The full verification run reported by the source was also private. The Squares Project independently built the statement closure and upper portion of the formalization, but as of October 7 has not independently replayed the entire formal proof, and it does not yet retain an external expert human review of that complete formalization. Those caveats are documented by the project.
That does not mean the result is fake.
Quite the opposite. The underlying optimality result has substantial independent computational and mathematical checking behind it.
It means there are different levels of the sentence:
“This has been verified.”
And we are going to need to get much better at distinguishing them.
Was an answer produced?
Was it numerically checked?
Was the mathematical argument independently reproduced?
Was it formalized?
Was the formalization independently compiled?
What assumptions and software sit inside the trusted computing base?
These distinctions used to live mostly in the weeds of computer-assisted mathematics.
If AI starts producing more mathematical results, they are going to become mainstream scientific literacy.
So did AI solve it?
This is probably the wrong question.
If by “AI solved it” we mean an autonomous model originated the problem, invented the entire method, generated the proof and independently verified itself without meaningful human involvement, then no.
If we respond by saying AI therefore did nothing important, that is also wrong.
Humans directed this work.
Humans supplied decades of prior mathematics.
Humans constructed the research infrastructure.
Humans evaluated and integrated the results.
And frontier models performed substantive mathematical work inside that process.
That last sentence would have sounded considerably more speculative not very long ago.
This is not AI replacing the mathematician.
It is also no longer merely AI acting as a fancy autocomplete for mathematical prose.
Something new is beginning to occupy the space between those two descriptions.
The eleven squares are almost beside the point
I do not particularly care about the optimal arrangement of eleven squares.
I mean, I care a little now, because after staring at Trump’s packing long enough I have developed a personal grudge against several of them.
But the larger significance is not the geometry.
It is the workflow.
We now have examples in which frontier language models are participating in mathematical exploration, helping construct arguments, reviewing reasoning, generating proof machinery and working alongside formal systems capable of checking at least substantial portions of the resulting work.
None of those pieces alone is revolutionary.
Together, they start looking like a research loop:
human direction → AI exploration → computational search → mathematical argument → formalization → mechanical verification → human review
The interesting question is what happens when that loop gets tighter.
What happens when the model proposing the lemma can immediately hand it to a proof assistant?
What happens when failure produces machine-readable counterexamples that go straight back into the reasoning process?
What happens when thousands of candidate approaches can be explored without thousands of mathematician-hours being spent on dead ends?
And what happens when these systems begin finding useful structures that humans did not think to search for?
We should absolutely resist the temptation to turn every computer-assisted theorem into AI DISCOVERS NEW MATHEMATICS in seventy-two-point type.
But we should resist the opposite temptation too: redefining every meaningful contribution downward until AI can never be said to have contributed anything.
The eleven-square result sits in that uncomfortable middle.
The AI did not wander into mathematics alone and return carrying fire.
But it was in the workshop.
It was using the tools.
And some of the things coming off the workbench are now theorems.
Leave a Reply