❯ Claude produces a machine-verified proof of a decades-old conjecture in percolation theory, not yet reviewed independently by mathematicians

The gap from 3 to 10 dimensionsIn late August, Anthropic technical staff member Justin Leder published on GitHub a proof completed autonomously by Claude models: on the square lattice in every dimension from two upward, percolation has no infinite connected cluster at the critical point. Previously this was proved only in two dimensions and in 11 and above, leaving dimensions 3 to 10 open. The result has drawn wide attention after recent media coverage.

What the question asksPercolation theory studies a grid where each edge is open with some probability, and asks how high that probability must be before a network spanning the whole appears. According to 36Kr, the problem was first posed by Broadbent and Hammersley in 1957 and has resisted solution for nearly 70 years. Hugo Duminil-Copin, a 2022 Fields Medalist, tried repeatedly; he wrote in an August 30 blog post that it was probably only a matter of time before the field’s most famous conjecture fell to AI.

Standing on a 2024 paperThe proof follows the approach of Gady Kozma and Shahaf Nitzan from 2024, who reduced the original conjecture to several conjectures about general graphs. Claude proved one of them and then applied their theorem to reach the conclusion. The argument is written in Lean 4 and checked step by step by computer. Gil Kalai wrote on his blog that the conjecture was so general that many expected a counterexample.

Checked by machine, not yet by peopleThe repository lists its own caveats: the proof has not been reviewed by independent mathematicians, all of the code and the 15-page guide were written by AI, and readers need to confirm for themselves that the formal definitions really express the original problem. Mathematician Kalai’s verdict is that “if verified, this will be an extraordinary breakthrough.” Benedikt Jahnel of Technische Universität Braunschweig told the press that a human who proved it would most likely win a Fields Medal.

▮ SIGNALA machine can guarantee that every step of the derivation is sound but not that the statement proved is the one people meant to ask, and checking whether the question was translated correctly is the mathematician’s new job in proofs like this.