Kozma and Nitzan (arXiv:2401.12397) reduced the statement \(\theta(p_c) = 0\) for Bernoulli bond percolation on \(\mathbb{Z}^d\), \(d \ge 2\), to an inequality on finite graphs, their Conjecture 3, and posed four further conjectures and four questions about connection probabilities in finite graphs: Conjectures 1, 2, 4 and 6 and Questions 5, 7, 8 and 9. Anthropic's Lean 4 / Mathlib proof of \(\theta(p_c) = 0\) for Bernoulli bond percolation on \(\mathbb{Z}^d\) in all dimensions \(d \ge 2\) (written by Claude under the direction of Justin Leder) proves Conjecture 3. It does not claim Conjecture 1, but Conjecture 1 is a relatively easy consequence of its intermediate first-contact inequality (GEN). That same result gives the stronger version retaining \(o\leftrightarrow A\) on the left, as explained below.
Here the remaining conjectures and questions of the paper are proved on top of that Lean proof: Conjectures 1, 2, 4 and 6 and Questions 5, 7 and 9, each in a stronger form than stated. Question 8 fails under the every-minimizer reading; the distinction matters when minimizers tie. The proofs are in the summary (PDF); the Lean files are in KNConjectures/ in the separate public repository.
In a companion page we prove, and check in Lean, that \(\theta(p_c) = 0\) for site percolation on \(\mathbb{Z}^d\) in every dimension \(d \ge 3\), from a single inequality about a finite family of independent hyperedges that yields bond percolation as well.
Notation
Throughout, \(G\) is a finite graph in which each edge \(e\) is open independently with probability \(p_e \in [0,1]\). For vertices \(x\) and \(y\), \(x \leftrightarrow y\) means that \(x\) and \(y\) are joined by a path of open edges, and \(C_x\) is the set of vertices joined to \(x\), the open cluster of \(x\). For a set \(A\) of vertices, \(o \leftrightarrow A\) means that \(o \leftrightarrow x\) for some \(x \in A\), and \(o \nleftrightarrow A\) is its negation. A comma inside a probability means intersection, \(\mathbb{P}(E, F) = \mathbb{P}(E \cap F)\), and \(\mathbb{E}[X;\, E]\) is the expectation of \(X\) on the event \(E\). Increasing functions \(F\) of vertex sets are those with \(F(K) \le F(L)\) whenever \(K \subseteq L\). All minima and convex combinations below use a nonempty set \(A\). Page numbers refer to the paper.
Conjecture 1 from the Lean proof of Conjecture 3
Fix \(A\), \(o\) and \(b\), and order the vertices of \(A\) so that \(\mathbb{P}(x \leftrightarrow b)\) is nondecreasing. Inequality (GEN) in the preceding proof, applied to \(F(K)=\mathbf1_{\{b\in K\}}\), gives \[ \sum_{x \in A} \mathbb{P}\bigl(o \leftrightarrow x \text{ and } o \nleftrightarrow y \text{ for every } y \in A \text{ before } x\bigr)\, \mathbb{P}(x \leftrightarrow b) \;\le\; \mathbb{P}(o \leftrightarrow b,\ o \leftrightarrow A). \] The events on the left partition \(\{o \leftrightarrow A\}\), and every factor \(\mathbb{P}(x \leftrightarrow b)\) is at least the minimum over \(A\), so \[ \mathbb{P}(o \leftrightarrow A)\, \min_{x \in A} \mathbb{P}(x \leftrightarrow b) \;\le\; \mathbb{P}(o \leftrightarrow b,\ o \leftrightarrow A). \] Dropping \(o\leftrightarrow A\) on the right gives Conjecture 1 (p. 3). Thus the stronger joint-event inequality already follows from the preceding bond proof, for every finite graph and every choice of edge probabilities.
The results
- Conjecture 4 (p. 32). Let \(F\) be an increasing function of vertex sets and let \(a \in A\) minimise \(\mathbb{E}\,F(C_x)\) over \(x \in A\). Then \(\mathbb{E}[F(C_a);\, o \leftrightarrow A] \le \mathbb{E}[F(C_o);\, o \leftrightarrow A]\). In particular \(\min_{x \in A} \mathbb{E}[F(C_x);\, o \leftrightarrow A] \le \mathbb{E}[F(C_o);\, o \leftrightarrow A]\), which is Conjecture 4; the same holds in the paper's formulation with a monotone cluster property \(f(v, \omega)\) in place of \(F(C_v)\).
- Conjecture 2 (p. 3), in the pre-FKG form (3): \(\min_{x \in A} \mathbb{P}(x \leftrightarrow b,\, o \leftrightarrow A) \le \mathbb{P}(o \leftrightarrow b,\, o \leftrightarrow A)\). Hence \(\min_{x \in A} \mathbb{P}(o \leftrightarrow A,\, x \leftrightarrow b) \le \mathbb{P}(o \leftrightarrow b)\), which is display (2).
- Question 7 (p. 36), answered yes. Let \(a \in A\) minimise \(\mathbb{P}(x \leftrightarrow b)\) over \(x \in A\). Then \(\mathbb{P}(o \leftrightarrow A,\, a \leftrightarrow b) \le \mathbb{P}(o \leftrightarrow b,\, o \leftrightarrow A)\), which is display (41).
- Conjecture 1 (p. 3), as above, and Conjecture 3 (p. 15) from it: for every \(\varepsilon > 0\) there is \(\delta > 0\) such that if \(\mathbb{P}(o \leftrightarrow A) > 1 - \delta\) and \(\mathbb{P}(x \leftrightarrow b) > 1 - \delta\) for every \(x \in A\), then \(\mathbb{P}(o \leftrightarrow b) > 1 - \varepsilon\).
- Question 5 (p. 32), answered yes. There are numbers \(c_a \ge 0\), \(a \in A\), with \(\sum_{a \in A} c_a = 1\), depending on \(G\), \(A\) and \(o\) but not on \(b\), such that \(\sum_{a \in A} c_a\, \mathbb{P}(o \leftrightarrow A,\, a \leftrightarrow b) \le \mathbb{P}(o \leftrightarrow b)\) for every vertex \(b\), which is display (38).
- Conjecture 6 (p. 34). Let \(e = \{v, w\}\) be an edge of \(G\), let \(a \in A\) minimise \(\mathbb{P}_G(x \leftrightarrow b)\) over \(x \in A\), and let \(G/e\) be the graph with the edge \(e\) shortened, that is, with the probability that \(e\) is open set to \(1\). Then \(\mathbb{P}_{G/e}(v \leftrightarrow b,\, v \leftrightarrow A) \ge \mathbb{P}_{G/e}(a \leftrightarrow b,\, v \leftrightarrow A)\), and therefore \(\mathbb{P}_{G/e}(v \leftrightarrow b) \ge \mathbb{P}_{G/e}(v \leftrightarrow A)\, \mathbb{P}_{G/e}(a \leftrightarrow b)\), which is display (40). The paper assumes in addition its display (39); that assumption is not needed, and it is in any case a consequence of Conjecture 1.
- Question 9 (p. 36), answered yes. Let \(H\) be \(G\) with every edge at \(o\) removed and let \(a \in A\) minimise \(\mathbb{P}_H(x \leftrightarrow b)\) over \(x \in A\). Then \(\mathbb{P}(o \leftrightarrow A,\, a \leftrightarrow b) \le \mathbb{P}(o \leftrightarrow b,\, o \leftrightarrow A)\) in \(G\).
- Question 8 (p. 36), which takes a vertex \(a \in A\) minimising \(\mathbb{P}(x \leftrightarrow b,\, o \nleftrightarrow A)\), fails if every minimizer must satisfy the proposed inequality. The counterexample has tied minimizers; it does not refute the existence of a suitable choice among them.
In the paper, Conjectures 2 and 4 are proved when \(A\) has two vertices (Theorems 1 and 7), when \(A\) has three vertices under extra hypotheses (Theorems 2, 3 and 11), when \(o\) is isolated in \(G \setminus A\) or joined only to \(A\) and to one further vertex (Theorems 4 and 5), and for the functions \(f = \mathbf{1}\{|C| \ge k\}\) with \(k \le 4\) on every graph (Theorem 9).
The method
The proofs run the argument of the Lean proof of Conjecture 3 with two changes. First, the clusters of the vertices of \(A\) are conditioned on missing a given set \(Y\) of vertices: if the vertices of \(A\) are ordered so that \(\mathbb{E}[F(C_x) \mid x \nleftrightarrow Y]\) is nondecreasing, then \[ \sum_{x \in A} \mathbb{P}\bigl(o \nleftrightarrow Y,\; o \leftrightarrow x,\; o \nleftrightarrow y \text{ for every } y \in A \text{ before } x\bigr)\, \mathbb{E}[F(C_x) \mid x \nleftrightarrow Y] \;\le\; \mathbb{E}[F(C_o);\; o \nleftrightarrow Y,\; o \leftrightarrow A]. \] Second, \(F(K)\) is replaced by \(F(K)\) minus the expectation of \(F\) at the cluster of \(a\) in the graph with every edge at a vertex of \(K\) removed; this new function is increasing in \(K\). Taking \(Y = \{a\}\) for the vertex \(a \in A\) minimising \(\mathbb{E}\,F(C_x)\) makes every conditional expectation on the left nonnegative, and the inequality becomes Conjecture 4 with the minimiser specified. The other conjectures and questions follow from that statement. For Conjecture 6 and Question 9 the cluster of \(o\) is replaced by the union of the clusters of a set of vertices: the union of the clusters of \(v\) and \(w\) does not depend on whether the edge \(\{v, w\}\) is open, and the cluster of \(o\) is the union of the clusters of \(o\) and of its open neighbours in the graph with the edges at \(o\) removed.
Implications
- The paper's chain of implications, Conjecture 4 to (3) to Conjecture 2 to Conjecture 1 to Conjecture 3 to \(\theta(p_c) = 0\), holds with every link proved, the last one in Anthropic's Lean proof.
- The vertex of \(A\) minimising \(\mathbb{P}(x \leftrightarrow b)\) is itself a valid choice in the pre-FKG comparison (Question 7), for every graph and every size of \(A\); so is the minimiser computed in the graph with the edges at \(o\) removed (Question 9).
- Conjecture 6 holds without its hypothesis (39), so the paper's Lemma 13 applies without it.
- The displayed inequality of the previous section holds with the union of the clusters of any finite set of vertices in place of \(C_o\), and it needs no sign condition on \(F\).
Files
| kn_summary.pdf | The summary: statements and proofs of all the results above. |
| KN-Conjectures | The Lean modules, build instructions, and
verification results.
The principal declarations use only propext, Classical.choice,
and Quot.sound, with no sorry. |
How to check
git clone https://github.com/nitromannitol/percolation-after-anthropic.git cd percolation-after-anthropic bash scripts/bootstrap.sh lake env lean scripts/Audit.lean
The repository pins Lean 4.32.0, Mathlib, and Anthropic's original proof. The default Lake build checks both parts, including all their retained Lean dependencies. See the README for the additional declaration checks and regression tests.
All of this was done autonomously by ChatGPT 5.6 Sol and Claude Fable 5.1, prompted by Ahmed Bou-Rabee, with minimal human intervention. Released under the Apache License 2.0, the licence of Anthropic's Lean proof.