Claude claims the percolation dying-conjecture; the experts are still checking the statement

In late August, an unusual document appeared inside Anthropic's public formal-math repository: a write-up of a claimed proof of the percolation dying-conjecture, a Lean verification of the argument, and a fifteen-page guide to the proof. There was no launch post, no model card, no announcement of any kind. Most of the field first heard about it from a blog post by Gil Kalai, a mathematician at the Hebrew University of Jerusalem, who flagged the claim on September 3 and described it in exactly those terms: a claim, not yet a result.

What the AI is said to have proved

Percolation is the study of networks whose connections open and close at random. Model the d-dimensional integer lattice as a grid of pipes, each open with probability p, and let theta(p) be the chance that a fixed point, say the origin, belongs to an infinite connected cluster. Below some threshold p_c that probability is zero; above it, positive. The dying-percolation conjecture is about the threshold itself: at exactly p_c, theta(p_c) equals zero, so even at the tipping point there is no infinite cluster. It had long been known for planar percolation and in high dimensions; the open case was the intermediate dimensions, beginning with dimension three.

The path the AI took was indirect. In January 2024, Gady Kozma and Shahaf Nitzan showed how to derive the dying-percolation conjecture from a broader conjecture about percolation on arbitrary finite weighted graphs, in a paper titled a reduction of the theta(p_c) = 0 problem to a conjectured inequality. Kalai noted at the time that their conjecture was so general that many mathematicians expected a counterexample to appear before long. The Claude document claims to prove that conjecture, which would settle theta(p_c) = 0 in every dimension at once.

A document, not an announcement

The artifact is a directory called percolation inside Anthropic's formal-math repository, holding a README, a bibliography, and summary.pdf, the guide. Anthropic has published no launch blog post for the result, and Kalai wrote that he thought it was "not yet an official Claude document (but I am not sure about it)." The README is unusually candid about its own status. It states that the work "has not yet been refereed by anyone independent of the author," that correctness rests on the mechanical checks it documents, and that readers should confirm for themselves that the statement file, Challenge.lean, "states the intended theorem."

The verification that is still running

In a machine-checked proof, the kernel verifies that every step follows from the axioms and from the definitions written in the file. It does not verify that those definitions express the theorem a mathematician had in mind. The mechanical apparatus can therefore do its job perfectly while the substantive question stays open, and that question, whether the formal statement means what the conjecture means, is the one experts are now working through. Kalai drew that line in a September 6 reply to a reader who asked what was left to verify.

"The new Lean verification is promising, but, as you said, we still need to verify if the formalisation is done correctly. There are still several issues with lean proofs, and, in any case, expert would like to see the details of the proof." — Gil Kalai

He added that "there are quite a few details which are still unprovided in order for experts to start digesting the new proof." His first assessment, posted three days earlier, was warmer, and it is the framing much of the field has adopted.

"A Claude document, accompanied with a Lean verification, claims a positive solution to the Kozma-Nitzan conjecture. ... If verified, this is a remarkable breakthrough." — Gil Kalai

In the same thread, Kalai noted that the remaining Kozma-Nitzan conjectures had also been proved, pointing to a separate verification page built on top of the same development.

The prediction that came three days early

On August 30, three days before the claim surfaced, the Fields medalist Hugo Duminil-Copin published an essay on the new blog Proofs and Prompts titled "Care for a little more AI?". He had worked on this precise conjecture early in his career and had not solved it, and he used it as his central example. It was, he wrote, "only a matter of time before the most famous conjecture in our field ... also falls to the bulldozers." He described a mathematical question as "much more than a theorem waiting to be proved," a "lighthouse in the night" that "illuminates and guides mathematicians."

Reaction since has been ambivalent rather than triumphant. Benedikt Jahnel of the Technical University of Braunschweig told Scientific American that "If someone manages to solve this problem, they'll probably receive a Fields Medal." On learning that an AI had, he said "The result evoked ambivalent feelings": joy that it was proved, and "a certain disillusionment that the final, crucial step came from an AI." He added that Fields Medals "have often, though not always, been awarded for proving theorems," and that "Whether a human being will ever make it onto such a list again is questionable."

That account carries its own footnote. Scientific American notes the piece first appeared in the German magazine Spektrum der Wissenschaft, and that its own English version was translated with the assistance of artificial intelligence and reviewed by human editors, which is the same division of labor the article is about.

What would settle it

Resolving this does not take a new proof. It takes an independent one. Three things would move the claim from a machine-checked artifact to a result the field can rely on. The first is an expert-verified exposition: the fifteen-page guide is, by the repository's own description, an aid to reading rather than the warrant, and its docstrings were machine-written and only filtered for release. The second is a review of the formalisation for statement fidelity, a human mathematician confirming that the definitions of the lattice, the open cluster and the critical probability say what everyone means by them. The third is replication: an outside group restating the theorem, or working the argument out by hand, and arriving at the same place.

What is already unusual is where the doubt now sits. The standard objection to an AI proof is that it might be wrong in the middle; here the middle is the part a kernel checked, and nobody is disputing that the file compiles. The open question is at the seam between the human statement and the formal one, and only mathematicians can answer it. That is the difference between this case and the ten-agent Lean proof of the Thomson problem at N=7 we covered on October 1: a closed, bounded statement whose cases could be enumerated and checked end to end. This one is an open problem whose difficulty is not the bookkeeping but whether the machine proved the conjecture at all. As we argued when an earlier AI-math result landed, the bottleneck is usually not producing a proof but finding enough mathematicians to read, check and absorb it, and here the checking is the entire story.