Claude-written Lean proof claims the dying percolation conjecture θ(p_c)=0 in every dimension
In early September 2026 a Lean 4 formalization written by Anthropic's Claude models (directed by Justin Leder, published in anthropics/formal-math) claimed to prove that critical Bernoulli bond percolation on Z^d has no infinite cluster for every d ≥ 2. It does this by proving a gluing inequality from Kozma–Nitzan (2024) that implies θ(p_c)=0. Gil Kalai called it "a remarkable breakthrough" if verified. Days later Ahmed Bou-Rabee, using GPT-5.6 Sol and Claude Fable 5.1, posted Lean proofs of stronger Kozma–Nitzan conjectures. No human referee has signed off yet.
Key facts
- Problem: θ(p_c)=0 (no percolation at criticality); previously known only for d = 2 and high dimensions (d ≥ 11). Open for 3 ≤ d ≤ 10
- Route: Kozma & Nitzan (arXiv 2401.12397, 2024) showed their Conjecture 3 ('near-one gluing') implies θ(p_c)=0 on Z^d for all d ≥ 2
- anthropics/formal-math percolation README: 247 Lean files, ~86,900 lines; axioms only propext, Classical.choice, Quot.sound; 'no human wrote or edited the Lean code'
- README caveat: 'has not yet been refereed by human mathematicians or by anyone independent of the author'
- Gil Kalai blog, 3 Sep 2026: 'If verified, this is a remarkable breakthrough'; he flags missing details in the written proof and the need to check the formalization
- Hugo Duminil-Copin had used θ(p_c)=0 as his main example in an essay on AI and mathematics a few days earlier
- Ahmed Bou-Rabee's verification page (updated 5 Sep 2026): Kozma–Nitzan Conjectures 1, 2, 4, 6 and Questions 5, 7, 9 proved in stronger form by 'ChatGPT 5.6 Sol and Claude Fable 5.1, prompted by Ahmed Bou-Rabee'; Question 8 fails under one reading
Science result
- Field
- mathematics / probability / percolation theory
- Problem
- Dying percolation conjecture θ(p_c)=0 for Bernoulli bond percolation on Z^d
- Result
- Claimed Lean-verified proof that θ(p_c)=0 for all d ≥ 2, via a new additive gluing inequality that settles Kozma–Nitzan Conjecture 3.
- AI system
- Claude (Anthropic), Claude Fable 5.1, GPT-5.6 Sol
- Human role
- Autonomous formalization: Claude wrote all the Lean code under Justin Leder's direction. The follow-up proofs of stronger conjectures were produced by GPT-5.6 Sol + Claude Fable 5.1 with 'minimal human intervention' from Ahmed Bou-Rabee
- Verification
- Formal proof in Lean (mechanically checked); the statement's fidelity and the informal write-up are not yet refereed
- Status
- pending
- Why surprising
- One of the central open problems of probability theory, which experts expected to need new ideas, was claimed through a machine-written 87k-line Lean development.
What happened
Kozma and Nitzan reduced the θ(p_c)=0 problem to an inequality about gluing connection events on finite graphs. In early September 2026 a Claude-written Lean development proved an additive form of that inequality. It went through a "conditioned slack hierarchy" of covariance inequalities, then applied Kozma–Nitzan's Theorem 6 to get θ(p_c)=0 in all dimensions d ≥ 2. Gil Kalai heard about it from Itai Benjamini and wrote it up on 3 Sep 2026. Separately, Ahmed Bou-Rabee published Lean proofs of several stronger Kozma–Nitzan conjectures, produced with GPT-5.6 Sol and Claude Fable 5.1.
The Wikipedia list credits the result to "Claude + Ahmed Bou-Rabee". The Anthropic repository itself credits Justin Leder as the director of the Claude run. Anthropic had not put out a press release as of late September 2026.
Why it matters
If the formal statement matches the intended theorem, a famous problem in mathematical physics is settled by machine-written formal mathematics. Commentators stress that Lean confirms the proof is correct but does not confirm the statement is the right one. Human experts still have to check that the formal definitions capture percolation on Z^d.
Changelog
- 2026-09-29: created
Related events
- Anthropic releases Claude Fable 5.1 and Claude Mythos 5.1 ★★★★★
- Claude produces the first complete machine-checked proof of Fermat's Last Theorem in Lean, in 11 days ★★★★★
- Claude proves more than two-thirds of Riemann zeta zeros are simple and on the critical line (up from 41.6%) ★★★★★
Sources (6)
- codeanthropics/formal-math: percolation README (commit 795efb8)
- discussionGil Kalai: Amazing: There is no Percolation at the Critical Probability in all Dimensions
- codeAhmed Bou-Rabee: Kozma–Nitzan conjectures verification page
- paperKozma & Nitzan: A reduction of the θ(p_c)=0 problem to a conjectured inequality (arXiv 2401.12397)
- discussionProofs and Prompts: Applied mathematics has met the machine before (on verification vs validation)
- discussionWikipedia: Dying percolation conjecture
id: 2026-09-03-dying-percolation-theta-pc-zero · updated 2026-09-29 · open in the interactive timeline