Percolation Theory Breakthrough: What Anthropic’s AI Actually Proved in Lean

A decades-old gap in percolation theory now has a machine-checked proof. Anthropic’s Claude models, working under mathematician Justin Leder’s direction, produced a Lean formalization proving that nearest-neighbour Bernoulli bond percolation on (\mathbb{Z}^d) does not percolate at the critical point for every dimension (d \ge 2). The previously unresolved cases were dimensions (3) through (10).

That sentence needs one important qualifier. The Lean development has passed mechanical checks, but the new proof has not yet been independently refereed by human mathematicians. Formal verification tells us that the theorem follows from the encoded definitions and proof steps. It does not, by itself, certify that the formal statement perfectly matches the intended informal mathematics.

Still, the result closes the previously unresolved dimensions (3) through (10), including the physically important three-dimensional case. The interesting part is not that an AI “found the percolation threshold.” It did not. The breakthrough concerns what happens exactly at that threshold, and it builds on a 2024 reduction by Gady Kozma and Shahaf Nitzan.

1. What Is Percolation Theory? A Simple Explanation

Percolation theory studies how large-scale connectivity emerges from many small random connections. Picture water moving through coffee grounds, fluid passing through porous rock, or a network where each link may be available or unavailable. The microscopic pieces are random, but the system can suddenly change from fragmented to connected.

In the standard mathematical model, the environment is represented as a graph. Vertices are locations, edges are possible connections, and each edge is independently declared open or closed. The central question is whether open edges can form a connected cluster that extends forever.

Here is the result at a glance:

That last point matters. The story is about the behavior of the system at criticality, not about computing a new numerical threshold.

2. How the Percolation Model Works

For Bernoulli bond percolation on the lattice (\mathbb{Z}^d), each nearest-neighbour edge is open with probability (p), independently of the others. If two vertices can be joined by a path made entirely of open edges, they belong to the same open cluster.

Pick the origin, usually written as (0). Let (C_0) be the open cluster containing it. The percolation probability is

[ \theta(p)=P_p(|C_0|=\infty). ]

In plain English, (\theta(p)) is the probability that the origin belongs to an infinite connected cluster.

The percolation threshold, or critical probability, is (p_c). It marks the boundary between a regime where an infinite cluster does not occur and one where it can occur.

Below (p_c), (\theta(p)=0). Above (p_c), (\theta(p)>0). The hard question was the knife-edge case: what happens exactly when (p=p_c)?

3. The Real Percolation Theory Problem Was at the Critical Point

The famous open problem can be written in one short equation:

[ \theta(p_c)=0? ]

If the answer is yes, then at the critical point there is almost surely no infinite cluster. The transition into the percolating phase happens continuously rather than by suddenly jumping to a positive probability of infinite connectivity.

This question had been open since at least the 1980s. Importantly, it is not the same as asking for an exact formula for (p_c). In fact, exact critical probabilities are notoriously difficult to obtain outside special cases. 2401.12397v1

For two-dimensional square-lattice bond percolation, the critical behavior was already understood. In sufficiently high dimensions, other methods also established (\theta(p_c)=0). The stubborn gap sat in between.

4. Why Dimensions 3 Through 10 Were the Missing Piece

Before this formal development, the critical-point result was known for (d=2) and for (d\ge11). The high-dimensional results came from techniques related to the lace expansion. That left dimensions (3,4,\dots,10) unresolved.

Three dimensions matter for an obvious reason: they are the closest mathematical analogue to connectivity in ordinary physical space. But the theoretical importance is broader. A proof covering every (d\ge2) removes an awkward dimensional hole from a foundational question about the percolation phase transition.

The Anthropic development proves the same statement uniformly for all dimensions (d\ge2). So the novelty is not a special trick for (d=3). It is a route that closes the entire missing range at once.

5. Kozma And Nitzan Reduced the Problem Before Claude Entered the Picture

The decisive setup came from a 2024 paper by Gady Kozma and Shahaf Nitzan. Rather than attack (\theta(p_c)=0) directly on the infinite lattice, they reframed the bottleneck as a finite-graph connectivity problem.

Their paper proposed several “gluing” inequalities. The idea is intuitive even if the probability statements are technical. Suppose one point (o) is very likely to connect to some point in a set (A), and every point in (A) is very likely to connect to another point (b). Can those strong local connection probabilities be glued into a strong probability that (o) connects to (b)?

The weakest form needed for their reduction was Conjecture 3. Roughly, for every target error (\varepsilon), there should be a tolerance (\delta) that works uniformly, regardless of how large the intermediary set (A) becomes.

That uniformity is the key. A naive union bound gets worse as (A) grows. Kozma and Nitzan showed that if Conjecture 3 were true, their Theorem 6 would imply

[ \theta(p_c)=0 ]

for (\mathbb{Z}^d) in every dimension (d\ge2).

So the 2024 paper did not solve the final problem. It identified a finite-graph inequality whose proof would unlock it.

6. What Anthropic’s AI Actually Proved

The new Lean development proves Kozma and Nitzan’s Conjecture 3, but it does so through a stronger statement called an additive gluing inequality.

If every (a\in A) satisfies

[ P(a\leftrightarrow b)\ge1-t, ]

then the development proves

[ P(o\leftrightarrow b)\ge P(o\leftrightarrow A)-t. ]

The striking feature is that the error term does not grow with the size of (A). That is exactly the kind of uniform control the renormalization argument needs.

From there, the logic is clean:

conditioned slack hierarchy → additive gluing → Kozma–Nitzan Conjecture 3 → Kozma–Nitzan Theorem 6 → (\theta(p_c)=0) for all (d\ge2).

The new underlying object is the conditioned slack hierarchy, a family of conditioned covariance inequalities for increasing functions of a single open cluster. Its level-zero unconditioned case connects back to the classical Harris inequality.

You do not need the full hierarchy to understand the significance. The important point is that the AI-produced proof did not merely restate Kozma and Nitzan’s reduction. It supplied a new finite-graph inequality strong enough to make that reduction work.

7. How Lean Checked the Percolation Theory Proof

Lean is a proof assistant. A mathematical argument written in Lean is broken into formal definitions and logical steps precise enough for a small trusted kernel to verify.

That is stronger than asking an AI model whether a proof “looks right.” The kernel does not grade style or plausibility. It checks whether each formal step follows from the accepted rules and previously established statements.

According to the project guide, the Lean 4 kernel accepts the development with no added axioms and no unsafe code. The only sorry placeholders are the two deliberate holes in the challenge statement file, not in the proved solution. The main theorems rely only on standard logical axioms used by Lean and Mathlib. Key compared theorems were also replayed through the independent nanoda kernel.

The project goes further than importing a large stack of unverified mathematical assumptions. Classical inputs used by the final argument, including Kozma and Nitzan’s reduction and other literature results, are re-proved inside the library from Mathlib foundations.

That gives the formal theorem a small trusted base. It does not eliminate the separate question of whether the encoded theorem is exactly the one mathematicians intended to settle.

8. Is the Percolation Theory Proof Really Verified?

“Verified” has two different meanings here, and mixing them creates most of the confusion.

At the formal level, the development is mechanically checked. Lean confirms that the theorem follows from the formal definitions and dependencies in the repository. The comparator check adds another layer by replaying key statements through a separate kernel.

At the mathematical-community level, independent review is still pending. The accompanying guide explicitly says that neither the development nor the guide has yet been refereed by human mathematicians or by anyone independent of the author. The review so far was performed by AI systems.

There is also a subtle formalization gap that responsible proof engineers always care about. A proof assistant can establish the theorem that was encoded. Humans must still inspect whether the definitions of the lattice, bond percolation, (\theta), (p_c), and the final proposition faithfully capture the intended mathematical statement.

So the careful description is: machine-checked, publicly inspectable, and not yet independently human-refereed.

That is more informative than either “AI solved it, case closed” or “it does not count until a journal accepts it.”

9. How Much Did Claude Do, And How Much Was Human-Steered?

The provenance is unusually explicit. Justin Leder’s guide says Anthropic’s Claude models wrote the Lean definitions, theorem statements, and proofs under his direction, and that no human wrote or edited the Lean code. The first drafts of the explanatory guide were produced in the same way.

That is substantial AI involvement. It is also not the same thing as an autonomous model independently choosing a famous open problem, inventing the research program, and publishing a proof without human direction.

The source material does not identify a specific Claude product version, so attaching the result to a particular model such as Opus or Sonnet would go beyond the evidence.

The most accurate picture is a human-directed AI research workflow. Human mathematicians had already isolated the bottleneck. Leder directed the formal project. Claude models produced the formal artifacts and the new proof machinery. Lean then checked the result.

That division of labor is arguably more interesting than the slogan “AI solves math,” because it shows where AI can fit inside real mathematical research rather than outside it.

10. What Anthropic’s AI Did Not Prove

The scope is narrower than some headlines may suggest.

The formalization did not produce a new exact value of the percolation threshold (p_c). It did not determine critical exponents. It did not establish the rate at which (\theta(p)) approaches zero near criticality. It also does not claim new results for general site percolation, arbitrary lattices, long-range models, or slabs.

Nor does it prove Kozma and Nitzan’s stronger Conjectures 1, 2, and 4 in general. The result targets the weakest gluing statement needed for the reduction, then proves something strong enough to imply it.

There is another technical nuance. Continuity of (\theta) on the full interval ([0,1]) is classically equivalent to the critical-point statement in this setting, but the formal release’s headline theorem is specifically (\theta(p_c)=0). That is the safest statement to repeat.

These limits do not diminish the result. They tell us exactly what changed and prevent a genuine theorem from being inflated into a broader claim.

11. Why This Result Matters for AI And Mathematics

For percolation theory, the immediate significance is straightforward: the formal development closes the dimensions that had remained open and gives a uniform theorem for nearest-neighbour Bernoulli bond percolation on (\mathbb{Z}^d) for every (d\ge2).

For AI, the more important lesson is methodological.

This was not a benchmark puzzle with a short hidden answer. The workflow involved a live research conjecture, a prior human reduction, new intermediate mathematical structure, a large formal library, and kernel-level verification. That is much closer to the messy shape of real research.

It also shows why formal mathematics is such a natural proving ground for advanced AI. Language models can propose definitions, lemmas, and proof strategies, while proof assistants enforce exactness. The model can be creative. The kernel can be unforgiving.

But formal verification changes the review problem rather than deleting it. Researchers still need to understand the theorem, inspect the modeling choices, compare the formal result with the intended claim, and decide whether the new machinery teaches us something reusable.

That may be where the most interesting human work moves next. Proving the theorem is one part of mathematics. Choosing the right problem, finding the right abstraction, explaining why the proof works, and connecting it to the rest of the field are different skills.

12. The Takeaway

The cleanest summary is not “Anthropic found the percolation threshold.” It did not.

The result is a machine-checked percolation theory proof that (\theta(p_c)=0) for nearest-neighbour Bernoulli bond percolation on (\mathbb{Z}^d) for every (d\ge2). The previously open dimensions (3) through (10) are covered. The proof works by establishing a new finite-graph inequality strong enough to prove Kozma and Nitzan’s Conjecture 3, which their 2024 reduction had already shown would settle the critical-point problem.

The formal evidence is unusually strong. The independent human mathematical review is not finished. Both facts belong in the headline-level understanding of the result.

For more source-driven explainers on AI research, formal mathematics, and the claims hiding behind the benchmarks, follow Binary Verse AI. We focus on what was actually proved, what was not, and why the difference matters.