OpenAI’s 2D area law proof Lean-verified by Axiom

OpenAI’s Oct 6 maths release (see the 722-manuscripts entry) included family 265, “Area laws and tensor networks for two-dimensional gapped systems”. Its paper “A two-dimensional area law from a global spectral gap” (dated Sept 24, 2026) claims an entropy area law for unique ground states of finite-range Hamiltonians on arbitrary finite induced subdomains of the square lattice, assuming only a uniform spectral gap of the full Hamiltonian and bounds on the local interactions. Unlike several other famous claims in the release, OpenAI’s catalogue gives no Lean link for this family.

On Oct 16 Axiom Math published AxiomMath/AreaLaw2D, which proves Theorem 1.1, Corollary 1.2 and all the exported intermediate propositions in Lean 4 with no sorry. The statement layer was written first and frozen. A separate challenge file restates the main theorem with every needed definition copied in, and the Lean comparator accepted the solution. According to the README, the proofs were “produced by Axiom’s agent tooling and OpenAI Codex, directed by Ruiz Chen, who froze and audited the statement layer and checked each result independently”. Parts of the supporting theory were ported from Sirui Lu’s TNLean and QICLean libraries. TNLean has its own partial, independent formalization of the same paper (Sections 2–4 and much of Section 11).

The commit history (HISTORY.md) shows Axiom’s internal quantum-arealaw library started in June 2026 with the Brandão–Horodecki 1D results. The OpenAI-specific work began on Oct 12 and the main theorem was finished by Oct 16. The working notes log every deviation from the paper’s conventions, for example a citation defect in a hypothesis docstring and the choice to prove over ℂ and transfer to any RCLike field.

No Axiom blog post, X announcement or Hacker News thread about the repo was found by Oct 18 evening. We found it through the sweep’s GitHub watch of AxiomMath.

Experts listed the 2D area law first among the “shocking” quantum claims in OpenAI’s release: Hastings proved the 1D case in 2007 and the general 2D gapped case has been open since. A full machine-checked proof removes doubt about the logic, though not about whether the formal statement matches the physics claim. That match rests on Axiom’s audited statement layer, which physicists can now read. It is also a case of AI agents verifying another lab’s AI-generated mathematics within weeks of publication.