Area laws and tensor networks for two-dimensional gapped systems

OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:

Proves an entropy area law for unique ground states of finite-range Hamiltonians on arbitrary finite induced square-lattice domains, using only a uniform full-system spectral gap and bounds on the local interactions. On open \(L\times L\) squares, uniformly gapped nearest-neighbor ground states also admit projected entangled-pair state approximations with polynomial bond dimension and global vector error at most L⁻¹.

The release has no Lean statement for this family, so there is no formal statement to compare with the result described above.

What the papers state

Theorem 1.1 (Area law)

In A two-dimensional area law from a global spectral gap, 24 September 2026

The paper’s main theorem is shown as a possible match to OpenAI’s description. No review confirming the selection is recorded.

For every q,R,J as above and every \Delta>0, there is a finite constant C=C(q,R,J,\Delta) with the following property. Suppose that \Lambda is a finite induced square-lattice domain and that the Hamiltonian (1.1) has a unique normalized ground vector \Omega, up to phase, with ground energy E_0, and satisfies

H-E_0\id\ \ge\ \Delta\bigl(\id-\ket{\Omega}\bra{\Omega}\bigr).

Then for every A\subseteq\Lambda,

S_\Omega(A)\le C\,|\partial_\Lambda A|.

The same constant applies to all such domains, sets, and Hamiltonians.

Corollary 1.2

In A two-dimensional area law from a global spectral gap, 24 September 2026

Possible match to OpenAI’s description, selected because it shares the most wording. No review confirming the selection is recorded.

The conclusion of Theorem 1.1 holds for every subset of a finite rectangular square lattice with bounded on-site and nearest-neighbor interactions and a unique ground state separated by a fixed global gap. For every domain covered by that theorem it also implies

S_\Omega(A)\le4C|\partial_{\rm in}A|, \qquad S_\Omega(A)\le2C|Z_A|.

The release does not say which paper theorem its catalogue describes. Both statements above are shown whole: the paper’s main theorem first, then the statement that shares the most wording with the description. The atlas has not reviewed either choice.

One more possible match

Theorem 1.1 in Polynomial PEPS approximation of gapped square-grid ground states, 24 September 2026.

Reported proof verification: The release has no Lean statement for this family. The papers are available to read and assess.
Papers and explanations: Two current papers, each readable here as a page beside its PDF. One explanation by others.

Papers

Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.

A two-dimensional area law from a global spectral gap

24 September 2026, current edition.

Read it here PDF

We prove an entropy area law for the unique ground state of a finite-range Hamiltonian on any finite induced subgraph of the square lattice. A lower bound on the spectral gap of the full Hamiltonian and fixed bounds on the local dimension, interaction range, and interaction strength suffice. For every set of sites, its entanglement entropy is bounded by a constant times the number of edges crossing its boundary, independently of the size and shape of the domain.

Polynomial PEPS approximation of gapped square-grid ground states

24 September 2026, current edition.

Read it here PDF

We prove that the unique ground state of a uniformly gapped nearest-neighbor Hamiltonian on an \(L\times L\) square lattice admits a projected entangled-pair state approximation with bond dimension polynomial in L and global vector error at most L⁻¹ after normalization. Only the gap of the full Hamiltonian is assumed. The result is an existence theorem, with constants uniform over Hamiltonians of fixed local dimension, interaction strength, and gap.

Lean statements

The release has no Lean statement for this family. Its papers remain available to read, and contributors can propose a formal statement of a result. Suggest a change

Independent comparisons and proof-verification reports

Does the Lean express the advertised result?

The release contains no Lean statement for this family, so there is no formal statement to compare with OpenAI’s description.

Other reports of proof verification

Other people’s accounts of running proof-verification software, with links to their reports.

LionSR, contributors, Area law and PEPS: provenance of imported OpenAI proofs (issue 8737), 7 October 2026. Source
Three pinned regression roots of the release built at adc7f124 with Lean 4.34.1 and locked Mathlib d13f23b7, with only propext, Classical.choice and Quot.sound, in TNLean CI run 37591286575.

Explanations by others

Explanations of this family written elsewhere, by the people named. Each is their own reading of the mathematics.

Yixin Ma, OpenAI mathematical physics, 25 families: a Chinese guided reading, 7 October 2026. Source
Chinese guided reading of this family that compares the manuscripts’ main theorems with their abstracts and flags boundary conditions and limit orders that change the physical reading; drafted with Codex and not a re-proof.

What these papers cite in the release, and what cites them

These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.

Within this family

Papers elsewhere in the release that this family’s papers cite

This family’s papers cite no paper elsewhere in the release.

Papers elsewhere in the release that cite this family’s papers

No paper elsewhere in the release cites this family’s papers.

References outside the release

Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release

Explain a result, compare statements or propose a correction

Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.

Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.

Offer to write an explanation Suggest a source attribution Suggest a change

What people have said

Commentary on this family by others, dated and credited. It is commentary, not a finding.

An unsigned public tier list, the OpenAI Math Tier List, classes it as a proof and rates its significance, if it holds up, as “Career-defining publication”. The page says that nothing on it is verified.
Author not stated. Source

Isaac Kim, Post listing quantum information results in the release, 6 October 2026. Source
Names 2D area law for gapped systems as a headline result.

Questions awaiting review

Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.

Identify the theorem the catalogue describes

Family 265 The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means. Open the form

State the result in Lean

Family 265 The release has no Lean statement for this family. Open the form