← All papers
On the proof of the Kozma-Nitzan conjecture
math.PR
Oct 21, 2026 · v1
TL;DR
Cites a third-party Lean 4/Mathlib formalization of θ(p_c)=0 for Bernoulli bond percolation on Z^d, the result the exposition concerns.
Abstract
In this short note, we give an exposition of the recent proof of the Kozma-Nitzan conjecture provided by OpenAI.
Problem
The Kozma-Nitzan conjecture concerns Bernoulli bond percolation, and a proof attributed to OpenAI was recently announced. The note aims to give a readable exposition of that proof.
Approach
The note presents the argument behind the announced proof in expository form. Its references include a Lean 4/Mathlib development by Justin Leder stating θ(p_c)=0 for Bernoulli bond percolation on Z^d in all dimensions d ≥ 2.
Results
The note gives an exposition of the proof. The supplied text shows a Lean formalization only through a citation and does not say how it relates to the exposition.