Most of the mathematics on this page was produced nearly autonomously by several versions of ChatGPT, which I prompted and directed. Each card names the models involved, states the result, and says what the model did and what I did. Each card also carries exactly one verification label. Lean-verified means Lean accepted a proof of the formal statement, using Mathlib alone, and the formal statement was checked against the statement written here. Checked by me means I read and checked the proof by hand. AI-generated means the model produced and audited the proof itself, and I have not yet checked it by hand.
The Kozma–Nitzan conjectures and \(\theta(p_c) = 0\) for site percolation
Lean-verifiedStatement
For Bernoulli bond percolation on \(\mathbb{Z}^d\), \(d \ge 2\), the probability \(\theta(p)\) that the origin lies in an infinite open cluster satisfies \(\theta(p_c) = 0\) at the critical probability, in every dimension. This is Kozma and Nitzan's Conjecture 3. The same conclusion, \(\theta(p_c) = 0\), also holds for Bernoulli site percolation on \(\mathbb{Z}^d\), \(d \ge 3\). Kozma and Nitzan's four further conjectures, Conjectures 1, 2, 4, and 6, and three of their four further questions, Questions 5, 7, and 9, are also proved, each in a form at least as strong as stated. Question 8 fails if every minimizer must satisfy the proposed inequality; the counterexample has tied minimizers, so a suitable choice among them may still exist.
Builds on
Anthropic's Lean proof that \(\theta(p_c) = 0\) for Bernoulli bond percolation on \(\mathbb{Z}^d\), produced by Claude under the direction of Justin Leder.
| Component | Proved by | Formalized in Lean by | Checked by |
|---|---|---|---|
| bond \(\theta(p_c) = 0\) | Claude (Anthropic), directed by Justin Leder | Claude (Anthropic), directed by Justin Leder | Lean (Mathlib) |
| Kozma–Nitzan conjectures and questions | ChatGPT 5.6 Sol (OpenAI), in about ten hours | Claude Fable 5.1 (Anthropic) | Lean (Mathlib) |
| site percolation via hypergraphs | ChatGPT 5.6 (OpenAI) | ChatGPT 5.6 (OpenAI), with Claude Opus 5 (Anthropic) and GLM 5.3 (Zhipu) | Lean (Mathlib) |
I directed the hypergraph extension and reviewed the resulting proofs and their Lean formalizations.