The margin, filled
Anthropic says a group of its Claude agents worked on their own for 11 days and came back with Fermat's last theorem written out in Lean, the language in which a computer can be made to check an argument step by step. The company puts the result at 13 million lines covering roughly 29,500 intermediate theorems, more than five times the 2 million lines gathered in Mathlib, the shared repository where formalised mathematics lives. Kevin Buzzard of Imperial College London, who had been running a five-year human effort on the same task, said the work leaves no assumptions beyond the axioms of mathematics.[1]
It helps to remember what that buys. Andrew Wiles announced his proof in 1993, a reader found a flaw in it, and repairing that flaw took him and Richard Taylor about a year. A proof assistant will not let a step through that it cannot derive, so the change here reaches who can vouch for the argument rather than what the argument says. Fermat's claim was true this time last week and it is true now. What is new is that a machine has walked the whole distance and found nothing missing.[1]
What the machine still needed
Put that beside a smaller result from the same week. Fifteen years ago Eric Harshbarger was asked for dice that would settle turn order fairly for any number of players, with no ties. He and a loose group around him cleared the three and four-player cases and then stopped. Harshbarger puts the space they were searching at about 10 to the power of 128 arrangements, which no amount of computing gets through by trying every option. The answer came in 2023 from Paul Meyer, a software engineer in Canada, whose program worked the patterns the group had already found in the four-player data: five 60-sided dice carrying every number from 1 to 300.[2]
The two stories share a shape. In each of them the machine came in after people had supplied the structure. The agents did not find a route to Fermat's theorem; they formalised the route Wiles and Taylor had already completed. Meyer's program did not outrun the search space; it entered through a door the group had cut into it with the four-player patterns. There is a deflationary reading of this, and it deserves saying: perhaps the difference is only how much computing each task had, since a formalisation has a written argument to follow line by line and the dice search had none. Even so, on the evidence in front of us, both machines started from a human floor.[1], [2]
What would make it shared ground?
Two days ago this column looked at the finished nervous system of a fruit fly and argued that a complete map turns an argument about behaviour into a lookup (A brain the size of a poppy seed, now readable end to end). The same test now arrives in mathematics, and it is harder here. A map is meant to be consulted; 13 million lines of Lean are meant to be trusted and then reused. An artefact that large earns its place only when other people can build on it, which is the thing Buzzard was pointing at when he called the algebra, harmonic analysis, geometry and number theory produced along the way robust enough to build on.[1], [3]
So there is a plain thing to watch, and it does not need anyone to guess how far this goes. If the formalisation is merged into Mathlib or imported by new Lean projects within the next six months, the claim that these artefacts are solid enough to build on will have a measurable footing, and the 2 million lines that repository holds today will be the yardstick. If it stands apart instead, admired and unused, it remains one demonstration by one company of what its agents can do in 11 days. Either way, a margin Fermat said was too small now has 13 million lines in it, and none of them are his.[1]