AI Solves Percolation Theory Problem: What Claude Proved in Lean

Mathematicians have a new headline to argue about: AI solves percolation theory problem that sat at the centre of probability theory for decades. Anthropic has published a formal proof, written by its Claude models, that critical percolation never produces an infinite cluster in any dimension from two upward. The result closes the famous open range from dimension 3 to 10. However, independent referees have not checked it yet.

The statement is short, which is part of why it became famous. Take an infinite grid in d dimensions. Open each edge at random with probability p, and close it otherwise. Then ask whether an endless connected path appears.

Below a critical value, called pc, every cluster stays finite. Above it, an infinite cluster shows up. The hard question was what happens exactly at pc. The new proof says the answer is nothing: at the critical point, the chance of an infinite cluster is zero. Experts write this as theta(pc) = 0.

That sounds technical, yet it carries a clean meaning. It says the phase transition is continuous. In other words, the network does not jump suddenly from broken to connected. It creeps up to the edge instead.

This question has a name: the dying percolation conjecture. First of all, two dimensions were settled long ago. Harry Kesten proved in 1980 that the critical value on the flat square grid is exactly one half, building on earlier work by Ted Harris.

Later, high dimensions fell too, thanks to a method called the lace expansion. Still, a stubborn gap remained in the middle, including the three dimensions we live in. Benjamini and co-authors called it the main long-standing open question in the field back in 1999.

Here is how the known cases lined up before September 2026.

The route ran through a 2024 paper by Gady Kozma and Shahaf Nitzan. They showed that the whole conjecture would follow from a set of inequalities about random connections on general graphs. Those inequalities were themselves unproven.

According to the project notes on GitHub, Claude proved one of them, known as Conjecture 3. It did so through a new chain of covariance bounds the files call a conditioned slack hierarchy. From there, the Kozma and Nitzan reduction delivers theta(pc) = 0 for every dimension from two upward.

Notably, the human name on the work is Justin Leder of Anthropic. His notes say Claude models wrote the Lean code autonomously under his direction, and that no human wrote or edited it. Gil Kalai flagged the claim on his blog on September 3, 2026.

The proof is not a PDF waiting for readers. Instead, it is a library for Lean 4, a proof assistant that checks every logical step by machine. Anthropic posted it in its formal-math repository.

The numbers give a sense of scale. For example, the project spans 247 Lean files and 86,892 non-blank lines. It uses only the three standard axioms of Lean and Mathlib, with nothing extra slipped in. On a 128-core Linux machine, the whole thing builds in about six minutes.

The library also re-proves the classic results it leans on, such as the Harris inequality and Kesten’s theorem. As a result, the chain from definitions to the final theorem sits inside one checked system.

Partly, and the difference matters. Lean has checked that the code proves the theorem as written. What no machine can confirm is whether those written definitions match the mathematics people intend.

The project says this plainly. Its notes state that nobody independent of the author has refereed the work so far, and they ask readers to inspect the statement file themselves. Kalai made the same point, writing that experts still need to verify whether the formalisation was done correctly.

In addition, there are limits on scope. The files do not claim Kozma and Nitzan’s other conjectures, site percolation, or other lattices. So the headline result is specific: bond percolation on the standard cubic grid.

Few people saw this coming as clearly as Hugo Duminil-Copin, the 2022 Fields Medalist who built much of modern percolation theory. On August 30, 2026, he published an essay warning that the field’s most famous conjecture would soon fall to what he called the bulldozers.

His worry was not about correctness. Rather, he argued that open problems act like lighthouses, guiding collaborations and side discoveries for years. Days later, the proof appeared.

Benedikt Jahnel of the Technical University of Braunschweig described mixed feelings to Scientific American. He said a person who solved it would probably have received a Fields Medal. He also felt joy at the proof, alongside disillusionment that the crucial step came from an AI.

Percolation is the maths of things leaking through random networks. For instance, think of water soaking through soil, coffee through grounds, or a fire jumping between trees. The same model describes a virus spreading across a city.

Knowing that the transition is continuous changes how scientists reason about those systems near their tipping point. Meanwhile, the bigger story is about method. In July, we covered how AI solved a math conjecture that had held out for 87 years. Now machine-checked proofs are reaching the problems experts treat as the core of their field.

If you want to try AI on your own papers and literature reviews, start with our guide to the best AI research tools. For the other big maths claim of the month, read how the OpenAI Navier Stokes proof sparked a credit fight.

Sources

Scientific American, Gil Kalai, Combinatorics and more, Anthropic formal-math on GitHub, Hugo Duminil-Copin, Proofs and Prompts, Kozma and Nitzan, arXiv, Wikipedia. *Photos: Kozma gady duminil-copin (Hugo Duminil-Copin, left, and Gady Kozma, Oberwolfach 2012) by Ivonne Vetter, CC BY-SA 2.0 DE, cropped and resized; 3D percolation by David Adams, CC BY 3.0, resized and placed on a white background.*