The century of the checker & will it matter for India’s story?

A machine has finished the most famous proof in mathematics in eleven days. The next decade belongs to whoever can tell the truth from output

Sometime around 1637, a French lawyer named Pierre de Fermat was reading a Greek textbook and had a thought. He noted it in the margin.

The claim was simple enough for a schoolchild. You can easily find whole numbers where 3² + 4² = 5². Try the same with cubes, or fourth powers, or anything above the square, and you will never find any. Then Fermat added the most famous sentence in the history of mathematics. He had discovered a marvellous proof, he wrote, but this margin was too narrow to contain it.

He was almost certainly wrong about having the proof. He was spectacularly right about the margin.

It took 358 years. Andrew Wiles finally settled it in 1995, and even then the first version had a hole in it that took another year and a collaborator to patch. What he produced was a document of well over a hundred pages, written in the compressed dialect of modern number theory, which perhaps a few hundred people on earth could genuinely evaluate. That is how mathematics has always worked. A proof is a piece of writing. It becomes true-for-the-community when enough qualified humans have read it and nodded. Last month, it has a change.

Eleven days

In the early hours of 7 August, a small team at the American AI lab Anthropic pointed several dozen copies of a language model at Wiles’s proof and asked it to write the whole thing out in a language called Lean. Eleven days later, working largely without human direction, the machines were done.

To understand what “writing it out” means, think about giving someone directions. A human mathematician writes directions the way a local gives them: take the second left after the temple, you can’t miss it. Everyone who knows the neighbourhood follows perfectly. Lean is not a local.

Lean is a machine that has never been to your city and refuses to take a single step you have not specified. Every “it follows that”, every “clearly”, every move a specialist would unpack silently in their head has to be written down and justified.

That is why a proof of a hundred-odd pages came out the other end at 13 million lines of code. Along the way the system proved 30,300 supporting statements, of which about 29,500 ended up in the final chain, and produced roughly six billion words of output. The finished object is more than five times the size of Mathlib, the shared library that the world’s Lean community has been assembling for over a decade. Lean then checked the entire structure and accepted it, relying on nothing beyond its three basic assumptions. A separate check confirmed that the thing proved was the real Fermat statement and not a convincing lookalike.

Kevin Buzzard, the Imperial College mathematician who in 2024 launched a five-year funded project to do exactly this job with human volunteers, called it extraordinary. He is not a man given to hype about machines.

Nobody is going to read it

Here is the part that should make you sit up. That 13-million-line file will never be read by a human being. Not skimmed, not spot-checked, not taught. It is not written for us. Its only reader is a program.

We have therefore arrived somewhere genuinely new: a mathematical certainty that no mind comprehends. For four hundred years, “we know this is true” and “somebody understands why” were the same sentence.

They have just come apart.

The instinct is to find this frightening. I think the more useful reaction is to ask where the trust went, because it did not disappear. It moved, and it got smaller.

Everything in that gigantic file rests on one small program at the centre of Lean called the kernel, a few thousand lines of code whose only job is to check that each step really follows. We have effectively swapped a jury of a hundred distracted experts for a single very careful judge. That is mostly an upgrade. It is also a concentration of risk, and concentrated risk fails in a particular way. Last summer, a soundness bug in that kernel briefly allowed a bogus “disproof” of a famous unsolved problem to sail through verification before anyone noticed. It was found and fixed. But it is worth saying plainly: machine-checked does not mean beyond doubt. It means the doubt has been squeezed into a smaller, more inspectable place.

A physicist’s confession

I should admit that in my own field this stopped being news around 1985.

Nobody reads a climate model line by line. Nobody reads the code behind a lattice simulation of the strong nuclear force, or the pipeline that turned raw detector counts into the Higgs boson. These are millions of lines written by hundreds of people across decades, and no single human has ever held one in their head.

Physics learned to live with it. We trust results by re-deriving them independently, by running rival implementations, by demanding that two groups who dislike each other get the same number, and by publishing an error bar on everything.

Mathematics was the last discipline where one person could, in principle, verify the whole chain personally. That was always its special dignity. It has now joined the rest of us, and it will need to import our habits: independent reimplementation, adversarial checking, and a culture that treats verified-but-unexplained as a real but partial kind of knowledge.

What the machine did not do

It did not discover anything. This matters, and the coverage has mostly missed it.

The system followed Wiles’s route. Its dependency graph closely tracks the original argument. It walked on a road that had been surveyed for it by an 86-page technical blueprint written by human mathematicians, over a decade of accumulated Mathlib groundwork, and a coordination tool built by a research group at Columbia. Its first attempt failed outright. Early runs collapsed because the parallel agents lost track of what had already been proved and kept redoing each other’s work.

So the honest sentence is not “AI proved Fermat’s Last Theorem in eleven days.” It is: the walking became astonishingly fast, and the map is still ours. Eleven days of machine time sits on top of twenty years of human scaffolding that nobody is going to write a headline about.

Which brings us to the real shift. A proof always did two jobs at once. It certified that something was true, and it explained why. Wiles’s proof gave number theory a whole way of thinking that mathematicians are still mining. The 13-million-line file teaches nobody anything. Those two jobs have now separated, and the machine has taken the cheaper one.

Why this is an Indian story

Every conversation about India and artificial intelligence eventually hits the same wall: chips, GPUs, power, capital expenditure, fabs, export controls. Formal verification is the one frontier where that wall does not exist. Lean is free. Mathlib is open. The coordination tools are open. The cost of entry is a laptop, a good teacher and time.

India produces mathematical talent at a rate few countries can match. It has almost no formal-methods community to speak of. That is not a resource problem. It is an attention problem, and attention is the cheapest thing a Government can redirect.

And this will not stay confined to mathematics for long. Within a decade, machine-generated claims will be arriving in drug dossiers, structural safety certificates, credit models, chip designs and Government statistics. Producing a claim is on its way to costing nothing. Checking one is not. A country that can generate but cannot verify will end up buying its certainty from abroad, exactly the way it once bought its electronics, and with far less ability to tell whether what it bought is sound.

So here is a small ask, A national formal-verification effort costing a few crore rupees, not a few thousand, seeded across IISc, the IITs, the Chennai Mathematical Institute, IMSc and TIFR, with two mandates: get Indian mathematics formalised and contributed upstream into Mathlib, and train a cohort of engineers who can formally verify safety-critical software. Set against Rs 1,27,500 crore for semiconductors, that is a rounding error on a rounding error. It is also the only line on India’s technology budget where we start level with everybody else.

Fermat complained that his margin was too narrow. We now know precisely how much room he needed: 13 million lines. What still does not fit in any margin, and never will, is the reason the thing is true.

The author is a physicist at the University of North Carolina at Chapel Hill and a contributor at Wall Street Journal; Views presented are personal.