Papers With

← All papers
First page of Notes on Kozma and Nitzan's proof of $θ(p_c)=0$

Notes on Kozma and Nitzan's proof of $θ(p_c)=0$

Arthur Blanc-Renaudie

math.PR Oct 7, 2026 · v1
formalization probability
Read PDF arXiv abstract
TL;DR
Gives a human-readable proof of Kozma–Nitzan inequalities whose AI-generated proofs were machine-checked in Lean 4/Mathlib; cites those Lean repositories.
Abstract
We present a human intelligible proof of the conjectures of Kozma and Nitzan, that they used to show $θ(p_c)=0$. The proof was recently found by AI, but was very poorly written. Our version is much shorter as it completely skips the horizontal term and its long estimate.
Problem

Kozma and Nitzan reduced θ(p_c)=0 for Bernoulli percolation on Z^d (d≥3) to a conjectured correlation inequality. An AI recently proved that inequality, but the result came as about 100,000 lines of Lean with poorly written manuscripts that were hard for probabilists to check.

Approach

The authors reconstruct a human-written proof from the AI's ideas, with their own notation. They use nested inductions on the sets A and B, linear projection operators π_{A,B}, covariance operators κ, and Harris's inequality with a Gibbs-type argument. They skip the 'horizontal term' and its long estimate.

Results

They obtain a self-contained proof of the Kozma–Nitzan conjectures that is roughly half the length of the original. Combined with Kozma and Nitzan's work, this yields θ(p_c)=0. The underlying result has Lean 4/Mathlib formalizations, which are cited.