Recently, Justin Leder released a remarkable Lean 4 development proving a long-standing conjecture in percolation theory (Leder 2026). The proof itself, as well as its Lean formalization, was generated by Anthropic’s Claude under Leder’s direction. If accepted after the usual mathematical scrutiny, it resolves a problem which had remained open for several decades, including the physically important case of three dimensions.
Let be an infinite graph and let . In Bernoulli bond percolation with parameter , every edge of is independently declared open with probability and closed with probability . We then study the connected components formed by the open edges, called open clusters.
The basic example is the lattice . Its vertices are the points and two vertices are joined by an edge when they differ by in exactly one coordinate.
Let be the probability that the open cluster containing the origin is infinite. Clearly is increasing in : opening more edges can only make connections easier.
There is a critical probability such that and Thus percolation exhibits a phase transition. Below all clusters are finite almost surely, while above an infinite cluster exists.
What happens exactly at
One might expect that the infinite cluster appears only after the critical point, so that But the definition of does not imply this. In principle, could jump from to a positive value at .
The problem of excluding such a jump became one of the central qualitative questions in percolation theory.
In dimension , Harris proved that (Harris 1960), while Kesten famously proved that (Kesten 1980). Hence
The situation in high dimensions was eventually understood using the lace expansion. Hara and Slade proved the required critical behaviour in sufficiently high dimensions (Hara and Slade 1990). Fitzner and van der Hofstad later pushed the method down to (Fitzner and Hofstad 2017).
Thus the dimensions remained open.
The new result closes this gap.
The route to the theorem is particularly interesting because the main new ingredient is not an estimate on itself.
In 2024, Gady Kozma and Shahaf Nitzan found a way to reduce the whole problem to an apparently elementary statement about percolation on finite graphs (Kozma and Nitzan 2024).
Consider a finite graph in which different edges may have different probabilities of being open. For vertices , write for the event that and are joined by an open path. If is a set of vertices, write when is connected to at least one vertex of .
Kozma and Nitzan conjectured the following “gluing” principle. For every , there should exist , independent of the graph and of the size of , such that and imply
At first sight this may seem obvious. If is almost certain to reach , and every point of is almost certain to reach , surely should almost certainly reach .
The difficulty is that may connect to any one of a huge number of vertices of . A naive union bound introduces an error proportional to , which is useless when is large. The remarkable content of the conjecture is that no such dependence on is necessary.
Kozma and Nitzan proved that this finite-graph statement alone implies simultaneously in every dimension .
Thus a famous infinite-lattice problem was reduced to a universal inequality about finite random graphs.
The 2026 Lean development proves this conjecture. In fact, the argument establishes the stronger additive inequality Consequently, if both probabilities in the assumptions above exceed , then Taking gives exactly the Kozma–Nitzan gluing conjecture.
There is an unusual aspect to the status of this theorem. The released proof is not merely a human proof subsequently translated into Lean. According to the project documentation, the mathematical argument, the definitions and the Lean proof were all generated by Claude under Leder’s direction. The Lean kernel verifies the formal derivation, and the project reports no additional axioms beyond the standard logical axioms used by Lean.
At the same time, the artifact has not yet undergone conventional independent mathematical refereeing. In particular, formal verification guarantees that the formal conclusion follows from the formal definitions and lemmas; human checking is still valuable to confirm that those definitions exactly represent the intended percolation problem and that the connection with the published Kozma–Nitzan reduction has been interpreted correctly.
Subject to that qualification, the result gives a remarkably clean answer to the original question:
Thus the phase transition for Bernoulli bond percolation on is continuous in every dimension. At the critical point there are clusters on arbitrarily large scales, but no infinite one.