AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

Critical bond and site percolation on the cubic lattice

Can the mathematical statement in Critical bond and site percolation on the cubic lattice be proved and verified machine-checked in Lean?

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)
Oct 6, 2026

Lean formalization in OpenAI math repository (Result 213)

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'Critical bond and site percolation on the cubic lattice'. We prove that nearest-neighbor Bernoulli bond and site percolation on ℤ3 have no infinite cluster at their respective critical parameters. The proof combines a finite connection inequality for independent hyperedges with a finite-scale extension estimate and an adaptive exploration.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 213). The Lean development was not rebuilt locally.