A Review Guide for the Formal Proof of Percolation Critical Probability

When mathematical open problems enter the realm of machine-checkable proofs, the evaluation focus shifts from “who announced the result first” to whether the proof object aligns with classical statements, whether each inference step is accepted by the proof assistant’s kernel, and whether gaps inserted by humans or models are hidden. A frequently discussed proposition in percolation theory can be summarized as: in bond percolation on the integer lattice, the probability of an infinite connected cluster occurring at the critical probability is zero. When formalizing this target, the lattice, edges, open edge configurations, probability measure, critical probability, and infinite cluster event must all be fixed. Otherwise, the subsequent “proven” result only holds for a different set of objects.

What the Proposition Actually States

Consider an integer lattice of dimension at least two. Each nearest-neighbor edge is independently and identically open or closed, with the open probability denoted as a parameter. The open cluster consists of vertices reachable from the origin along open edges. If this cluster is an infinite set with positive probability, percolation is said to occur. The percolation probability is the probability of this event, which is monotonically non-decreasing with respect to the open probability. The critical probability is the threshold where the percolation probability transitions from zero to positive. The target proposition is: exactly at this threshold, the percolation probability remains zero. Different dimensions, bond versus site percolation, and nearest-neighbor versus long-range connections will all alter the proof path. During review, one cannot secretly replace “continuity in a certain dimension” with “probability zero at the critical point across all dimensions.”

This distinction defines the acceptance scope. If the material’s title or module comments fluctuate between “3D continuity,” “critical point disappearance in all dimensions,” and “just scaffolding,” it should be regarded as an unfrozen scope, not a writing issue. A formalization project should use the finally derived theorem statement as the sole contract: premises, dimension constraints, percolation type, and conclusions must be verbatim readable in the same file.

Freeze Objects Before Reviewing

Reliable reviews follow this sequence, rather than just looking at how long the proof is.

First, the lattice and edge set. The vertex set, allowed edges, and translation invariance must align with textbook models. Treating approximations on a finite box as events on an infinite lattice, or writing periodic boundaries into the “infinite cluster,” will cause the meaning of critical probability to drift.

Second, the configuration space and probability. The open edge configuration is typically a product space over the edge set, and the measure is a Bernoulli product measure. It must be confirmed that properties relied upon by subsequent lemmas, such as monotonicity and translation ergodicity, are actually derived from this definition, not merely assumed in comments.

Third, the definition of critical probability. The common formulation is the infimum where the percolation probability becomes positive. If equivalent characterizations like “the limit of the finite-size crossing ratio” or “the divergence point of the average cluster size” are introduced, an equivalence proof must be provided. One cannot place two symbols side by side and assume they are identical.

Fourth, the infinite cluster event. The event should be expressed as: for any radius, the open cluster of the origin intersects outside that radius, or as an equivalent countable union and intersection. It must be verified that it belongs to the measurable sets, and that when exchanging the order of monotonic limits with finite box events, a permitted convergence theorem is used.

An illustrative acceptance checklist can be recorded in plain text, without relying on a specific repository interface:

Proposition identifier, dimension conditions, percolation type, measure parameters, critical probability definition, target event, full name of the derived theorem, whether it relies on additional axioms, location of unfinished placeholders, and verbatim consistency with the challenge statement.

Challenge Statements and Solutions Must Align

Mature formalization workflows separate “what to prove” from “how to prove it.” The challenge file only provides definitions and theorem signatures, while the solution file provides the proof term. During review, the two statements should be compared verbatim: types, implicit parameters, classic axiom packages, and namespaces all count as differences. If a solution passes the check by relaxing premises, strengthening the negation of the conclusion, or turning the theorem into a conditional lemma, it has not solved the original problem.

Similarly, one must search for unfinished proof placeholders and additional axioms. A placeholder means the kernel did not check that branch; if a newly added axiom is equivalent to the target itself or to an unformalized analytical estimate, the entire development has merely moved the difficulty elsewhere. The allowed foundation is the logic and mathematical library already accepted in the proof assistant, not a temporary declaration of “obvious” made for this specific target.

Build records should preserve the version identifier that passed kernel checks, dependency locks, and logs. Simply keeping an oral statement that “it passed locally” is insufficient. If the outside world can only see the source code snapshot but not a repeatable check log, the conclusion should be stated as “static review found no obvious gaps,” rather than “the theorem has been verified by the community.”

What AI Assistance Excels At and What It Cannot Replace

Large language models (LLMs) are well-suited for retrieving lemma names, generating boilerplate structures, translating natural language estimates into proof scripts, and making local patches based on type error logs. Common modules in percolation proofs include: increasing events, correlation inequalities, renormalization or box-crossing estimates, and limits from finite scales to infinite volumes. Models can accelerate the connection of these templates, but whether the constants in correlation inequalities, dimension conditions, and boundary terms are correctly instantiated must be jointly vetted by type checking and human reading.

A practical division of labor is: humans are responsible for freezing the mathematical model and writing theorem signatures that cannot be altered; models fill in the proofs; automated checks reject placeholders and type errors; and an independent round of reading compares against definitions in classical literature, rather than the model’s own summary. Two rounds of independent static review that agree on file size, placeholder locations, and axiom scans can only increase the credibility of “no obvious text-level loopholes,” but cannot replace the judgment of whether the mathematical idea is correct. If a conceptual error is absorbed by an incorrect definition, type checking will still pass.

Therefore, evaluating such work should adopt a tiered conclusion system. Tier 1: Object definitions align with the target proposition, no placeholders, no additional axioms, and check logs are repeatable. Tier 2: The proof structure covers the expected analytical steps, and the premises of key estimates match the dimensions. Tier 3: Compared to existing proof routes in the literature, does it provide a new argument rather than just transcribing a known proof? If Tier 1 is not reached, it is inappropriate to publicly claim the problem is solved.

Details Prone to Distortion in Probability Formalization

Percolation is not pure combinatorial counting. The following points are most likely to slip in generative proofs.

Monotone coupling. Different open probabilities should be compared in the same probability space; otherwise, “no percolation below critical probability, percolation above it” cannot be transferred between variables.

Tail events and the zero-one law. The occurrence of an infinite cluster is often related to translation-invariant tail events. If the premise of the zero-one law requires the event to belong to the tail sigma-algebra, one must prove that the written event indeed belongs to it, rather than invoking the law just because the word “infinite” is in its name.

Finite approximation. Crossings within boxes, arm events, and scale iterations are estimation tools, not the target event itself. Deducing “percolation probability is zero at the critical point” from “crossings occur with probability close to one at every scale” requires union bounds, convergent summation, and parameters falling within the critical window in between. Missing any step, type checking might still pass due to an axiom placeholder.

Measurability and integration exchange. The monotone convergence of expectations and the smoothing of conditional expectations must correspond to proven theorems, not remain in comments.

An illustrative structure can be written as a pseudo-code proof skeleton for division of labor, but a skeleton is not a proof:

Define the configuration measure and percolation probability function; prove the function is monotonic; define the critical probability; prove the probability is zero below the critical value; use scale iteration at the critical value to prove the infinite cluster probability is still zero; derive the theorem. Only after the type signatures of each step are frozen is filling permitted.

Publication, Retraction, and Evidence Boundaries

In engineering, it is common for source code to be briefly visible, then marked as unfinished, and the merge closed. What the outside world can confirm is only observable behavior: the file existed, the statement was renamed, and it ultimately did not enter the stable branch. One cannot infer from “it once appeared” that the lab internally approved it, nor from “it was later closed” that the proof is necessarily wrong. A responsible expression presents parallel evidence: visible theorem statements, placeholder and axiom scans, whether check logs exist, and whether the stable branch includes it.

If enterprises want to productize similar workflows, they should put proof objects, check records, and review opinions into a traceable artifact repository, use object storage to save snapshots, use continuous builds to run kernel checks, and use permissions and audit logs to restrict unreviewed results from being externally visible. These are general engineering capabilities that do not depend on any specific model or one-off public exposure. Intelligent programming tools can participate in drafting, but the merge gate must be deterministic proof checking, not a conversation record.

How to Form Your Own Judgment

Readers do not need to take sides with a particular research group. The actionable judgment is: is the proposition exactly that the percolation probability is zero at the critical probability; are dimensions and percolation types fully specified; are the measure, critical value, and infinite cluster self-consistent; are the challenge and solution the exact same statement; are there placeholders and additional axioms; is the check repeatable. Only when all five are satisfied is it worth having mathematical experts further review whether the route itself is novel and correct. If any is unmet, it remains a draft or scaffolding.

The value of formalization lies in pulling the debate back from rhetoric to objects. Rigorous proofs of critical percolation behavior have historically relied on fine estimates, and AI assistance will only make drafts appear faster. Faster drafts require stricter freezing, comparison, and gating, not louder announcements. Writing the acceptance criteria clearly is itself the most useful engineering response to this classic problem.