Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Show on the map

Spacetime Penrose inequalities: enclosing area, charge, rotation, and anti-de Sitter extensions

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

Proves the sharp enclosing-area spacetime Penrose inequality for smooth one-ended asymptotically flat initial data in every spatial dimension n ≥ 3, under dominant energy, weak future trapping, positive enclosing area, and the stated decay assumptions. It bounds invariant ADM mass below using minimum enclosing area, with equality rigidity under additional horizon hypotheses. Charged upper-area bounds treat dyonic three-dimensional data; the higher-dimensional purely electric extension uses the matched neutral theorem. (OpenAI’s Lean note)

Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.

The independent assessments find that the Lean statements express a supporting step or a different result. Read the assessments

What the papers state

Theorem 2.2 (Penrose inequality and nondegenerate rigidity)

In The Kerr–Newman Penrose Inequality for Axisymmetric Electrovacuum Exteriors, 5 October 2026

Possible match to OpenAI’s description, selected from shared wording. No review confirming the selection is recorded.

Under the hypotheses of this section,

\boxed{\displaystyle m^2\ge\frac{A}{16\pi}+\frac{Q^2}{2} +\frac{\pi(Q^4+4J^2)}A.}

If A>4\pi\sqrt{Q^4+4J^2} and equality holds, the original exterior (\Omega,g,K,E_{\mathrm f},B_{\mathrm f}) admits a smooth spacelike embedding into the domain of outer communication together with the appropriate future horizon of a subextremal dyonic Kerr–Newman spacetime with mass m, angular momentum J, and charges Q_e,Q_b, in the conventions above. The induced metric, second fundamental form with a consistent future normal, and induced fields agree with the given data. The end approaches the corresponding spatial infinity. The embedding and normal extend smoothly to S, which maps to a smooth future-horizon cross-section or to the bifurcation sphere.

Conversely, every such Kerr–Newman exterior slice satisfying all the hypotheses and meeting that horizon attains equality. Nonconstant time graphs and nonzero second fundamental forms are permitted.

No Lean statement in the release is paired with this theorem.

Theorem 1.2 (Global maximal AH Penrose inequality)

In The Penrose inequality for maximal asymptotically hyperbolic initial data, 5 October 2026

Possible match to OpenAI’s description, selected from shared wording. No review confirming the selection is recorded.

Under (1.2)–(1.8), the completeness, one-end, and smoothness assumptions above, and the future-timelike condition (1.5), one has

m_{\AH}(g)\ge\frac12\bigl(r_A+r_A^3\bigr), \qquad r_A=\sqrt{\frac{A_{\min}(S;g)}{4\pi}}.

The coefficient is sharp: equality holds for every positive-mass time-symmetric Schwarzschild–anti-de Sitter exterior bounded by its minimal horizon.

No Lean statement in the release is paired with this theorem.

The release does not say which paper theorem its catalogue describes. The statements above share the most wording with the description; the atlas has not reviewed that choice. Identifying it is listed under Questions awaiting review.

30 more possible matches

  • Theorem 2.7 (Original-data rigidity) in A Charged Reduction of the Spacetime Penrose Inequality in Spatial Dimensions at Least Four, 5 October 2026.
  • Theorem 16.1 in Boundary graph deformations for the spacetime Penrose inequality, 27 September 2026.
  • Theorem 2.3 (Numerical input) in Equality and rigidity in the spacetime Penrose inequality, 27 September 2026.
  • Theorem 2.6 (Converse and sharpness) in The spacetime Penrose inequality with charge and original-data rigidity, 5 October 2026.
  • Theorem 2.5 (Purely electric spacetime Penrose inequality) in A Charged Reduction of the Spacetime Penrose Inequality in Spatial Dimensions at Least Four, 5 October 2026.
  • Theorem 8.2 (Four-dimensional boundary deformation) in Boundary graph deformations for the spacetime Penrose inequality, 27 September 2026.
  • Theorem 2.6 (Converse and sharpness) in Equality and rigidity in the spacetime Penrose inequality, 27 September 2026.
  • Theorem 6.2 (Neutral deformation with a prescribed loss) in The Kerr–Newman Penrose Inequality for Axisymmetric Electrovacuum Exteriors, 5 October 2026.
  • Theorem 1.2 (Original-data equality) in The nonmaximal anti-de Sitter Penrose Inequality and original-data rigidity, 5 October 2026.
  • Theorem 2.5 (Original-data equality) in The spacetime Penrose inequality with charge and original-data rigidity, 5 October 2026.
  • Theorem (number unavailable) (MOTS barriers and the total trapped region) in Boundary graph deformations for the spacetime Penrose inequality, 27 September 2026.
  • Theorem 2.5 (Original-data rigidity) in Equality and rigidity in the spacetime Penrose inequality, 27 September 2026.
  • Theorem 4.1 (MOTS barriers and the total trapped region) in Spacetime Penrose inequalities, 5 October 2026.
  • Theorem 1.3 (The enclosing-area Penrose inequality) in The spacetime Penrose inequality and enclosing area, 27 September 2026.
  • Theorem (number unavailable) (Minimum-enclosing-area inequality) in Boundary graph deformations for the spacetime Penrose inequality, 27 September 2026.
  • Theorem 2.2 (Minimum-enclosing-area inequality) in Spacetime Penrose inequalities, 5 October 2026.
  • Theorem 2.4 (Neutral numerical input) in A Charged Reduction of the Spacetime Penrose Inequality in Spatial Dimensions at Least Four, 5 October 2026.
  • Theorem 2.1 in A local Penrose inequality for conformal perturbations of Schwarzschild–anti-de Sitter data, 5 October 2026.
  • Corollary 1.2 (Sharp Bondi inequality in the CKS class) in Area-controlled end replacement and the Bondi Penrose inequality in the CKS class, 27 September 2026.
  • Theorem 1.1 (Area-controlled end replacement) in Area-controlled end replacement and the Bondi Penrose inequality in the CKS class, 27 September 2026.
  • Theorem 12.1 (Measurable axial coefficient) in Boundary graph deformations for the spacetime Penrose inequality, 27 September 2026.
  • Theorem 1.1 (Nonmaximal anti-de Sitter Penrose Inequality) in The nonmaximal anti-de Sitter Penrose Inequality and original-data rigidity, 5 October 2026.
  • Corollary 1.4 (Automatic future timelikeness in the strong-decay class) in The spacetime Penrose inequality and enclosing area, 27 September 2026.
  • Theorem 1.5 (Weaker decay in dimensions three and four) in The spacetime Penrose inequality and enclosing area, 27 September 2026.
  • Theorem 2.3 (Charged spacetime Penrose inequality) in The spacetime Penrose inequality with charge and original-data rigidity, 5 October 2026.
  • Theorem (number unavailable) (Three-dimensional boundary deformation) in Boundary graph deformations for the spacetime Penrose inequality, 27 September 2026.
  • Theorem 1.1 (Riemannian Penrose inequality with minimizing frontiers) in Conformal flow and the Riemannian Penrose inequality with minimizing frontiers, 27 September 2026.
  • Theorem 1.1 in Electromagnetic tails and the Kerr–Newman Penrose inequality, 5 October 2026.
  • Theorem 7.5 (Existence on finite truncations) in Spacetime Penrose inequalities, 5 October 2026.
  • Theorem 1.3 (Time-symmetric time-component inequality) in The Penrose inequality for maximal asymptotically hyperbolic initial data, 5 October 2026.
Reported proof verification
One Lean statement in the release; two independent groups report that Comparator accepted runs for this file at the version shown here.

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.

The spacetime Penrose inequality with charge and original-data rigidity

5 October 2026, current edition.

Read it herePDF

Under the stated energy, decay, and trapping hypotheses, we prove the sharp charged spacetime Penrose upper-area inequality for one-ended three-dimensional initial data with source-free electric and magnetic fields. The theorem allows arbitrary second fundamental form, nonzero ADM momentum, and disconnected boundary. Writing m for invariant ADM mass, Q for total charge magnitude, and rA for the minimum-enclosing-area radius, the bound is m ≥ Q and \(r_A\le m+\sqrt{m^2-Q^2}\). The polynomial mass bound \(m\ge(r_A+Q^2/r_A)/2\) is asserted only when \(r_A\gt Q\). When m > Q, equality under the stated connected, outermost, outer-area-minimizing future-horizon hypotheses identifies the original data as a smooth spacelike slice of dyonic Reissner–Nordström, including smooth attachment at the future horizon.

A Charged Reduction of the Spacetime Penrose Inequality in Spatial Dimensions at Least Four

5 October 2026, current edition.

Read it herePDF

Using the companion neutral spacetime Penrose theorem exactly at its stated strong-decay, future-trapped, positive-area, and future-timelike scope, we prove the sharp purely electric upper-area inequality in every spatial dimension n ≥ 4 for one-ended charged data satisfying the charged dominant energy condition and \(\mathop{\mathrm{div}}\nolimits _g E=0\), with the specified decay, integrability, and finite-flux assumptions. The data may have arbitrary interior topology and ADM momentum, with a future or past trapping sign chosen independently on each boundary component. Positive enclosing area and strict ADM timelikeness are conclusions. The polynomial mass rearrangement is asserted only when the \((n-2)\)nd power of the enclosing-area radius exceeds \(|Q|\). When \(m\gt |Q|\), equality under the stated connected, outermost, outer-area-minimizing future-horizon hypotheses recovers the original metric, second fundamental form, and electric field as a global spacelike slice of a Reissner–Nordström–Tangherlini exterior. The equality classification includes only slices whose induced magnetic two-form vanishes.

Spacetime Penrose inequalities: enclosing area, charge, and rigidity

5 October 2026, current edition.

Read it herePDF

We prove sharp spacetime Penrose inequalities for invariant ADM mass and minimum enclosing area in three and four spatial dimensions. Under their respective designated-end conventions, the neutral numerical results allow arbitrary second fundamental form, nonzero momentum, disconnected weakly future trapped boundary, and finitely many ends. Under the stated horizon hypotheses, equality for the neutral inequalities reconstructs the original exterior data as spacelike slices of Schwarzschild spacetime in three dimensions and Schwarzschild–Tangherlini spacetime in four; the four-dimensional equality theorem concerns a connected, one-ended exterior. We also prove a three-dimensional electric–magnetic charged upper-area inequality for one-ended data with nonzero momentum, with separate purely electric rest-frame corollaries allowing finitely many ends. Finally, for each fixed transverse-traceless seed and prescribed decaying solution branch, we prove a local Schwarzschild–anti-de Sitter inequality.

The Kerr–Newman Penrose Inequality for Axisymmetric Electrovacuum Exteriors

5 October 2026, current edition.

Read it herePDF

We prove the sharp Kerr–Newman Penrose inequality \(\displaystyle m^2\ge \frac{A}{16\pi}+\frac{Q^2}{2} +\frac{\pi(Q^4+4J^2)}{A}.\) Here \(Q^2=Q_e^2+Q_b^2\), and J is the conserved total angular momentum, including its electromagnetic contribution. The result applies to smooth axisymmetric electrovacuum exteriors in the stated one-ended topological and decay class, with a connected outermost, outer-area-minimizing future marginally outer trapped boundary, Coulomb electromagnetic asymptotics, zero ADM momentum, and the explicitly assumed physical-area condition \(A\ge4\pi\sqrt{Q^4+4J^2}\). No maximality assumption is made. On the strict area branch, equality within this class characterizes the original data as an admissible spacelike exterior slice of a subextremal dyonic Kerr–Newman spacetime, with the boundary mapped smoothly to a future-horizon cross-section or the bifurcation sphere.

Electromagnetic tails and the Kerr–Newman Penrose inequality

5 October 2026, current edition.

Read it herePDF

We construct smooth axisymmetric electrovacuum exteriors that violate the Kerr–Newman Penrose inequality when J is the bare gravitational ADM angular momentum and the electromagnetic fields have only \(O(r^{-2})\) decay, allowing angularly varying leading tails. The examples have zero total electric and magnetic charge even though both electromagnetic fields are nonzero. They have a connected outermost, outer-area-minimizing future marginally outer trapped boundary and lie strictly on the physical area branch. We also obtain equality examples whose original data admit no Kerr–Newman spacelike realization with the corresponding mass, angular momentum, and charges. These counterexamples do not refute formulations using conserved total angular momentum with its electromagnetic correction or stronger Coulomb asymptotics.

The nonmaximal anti-de Sitter Penrose Inequality and original-data rigidity

5 October 2026, current edition.

Read it herePDF

We prove the spacetime Penrose Inequality for smooth three-dimensional initial-data exteriors with one spherical asymptotically anti-de Sitter end, satisfying the stated decay and integrability assumptions, the dominant energy condition, and a compact weakly future outer trapped boundary. We assume that the hyperbolic metric four-flux is future timelike; its Lorentz norm is the mass, and the area is the infimum over full enclosing cuts. On the connected outermost, outer area-minimizing horizon subclass, equality characterizes the original data as a spacelike hypersurface in Schwarzschild–anti-de Sitter spacetime with matching metric mass. No maximality, evolution, or auxiliary solvability assumption is used.

The Penrose inequality for maximal asymptotically hyperbolic initial data

5 October 2026, current edition.

Read it herePDF

We prove the sharp Penrose inequality for three-dimensional maximal asymptotically hyperbolic initial data with spherical conformal infinity. Under the dominant energy condition, the stated decay and integrability assumptions, and a future-timelike mass covector, the invariant mass is bounded below by the Schwarzschild–anti-de Sitter mass associated with the minimum enclosing area of a weakly future outer-trapped boundary. The boundary may be disconnected, and no restriction is imposed on the compact topology.

A local Penrose inequality for conformal perturbations of Schwarzschild–anti-de Sitter data

5 October 2026, current edition.

Read it herePDF

We prove the asymptotically hyperbolic Penrose inequality for sufficiently small maximal vacuum conformal perturbations of a positive-mass Schwarzschild–anti-de Sitter exterior, for every fixed decaying transverse-traceless seed and every solution branch satisfying the stated decay and mass assumptions. The bound uses the area of the marginally outer trapped boundary itself; it requires neither outermostness nor outer area-minimization, and no bulk-versus-boundary domination condition. For sufficiently small positive parameters, equality holds for radial seeds and the inequality is strict otherwise.

The spacetime Penrose inequality and enclosing area

27 September 2026, current edition.

Read it herePDF

We prove the sharp spacetime Penrose inequality for smooth one-ended initial-data exteriors in every spatial dimension n ≥ 3, under the dominant energy condition, weak future trapping, the stated differentiated decay and positive enclosing area. These hypotheses force the ADM energy-momentum to be future timelike. Area is the infimum over full enclosing cuts in the original metric. In dimensions three and four, two metric derivatives and one tensor derivative suffice, and both positive enclosing area and future timelikeness follow from the hypotheses.

Conformal flow and the Riemannian Penrose inequality with minimizing frontiers

27 September 2026, current edition.

Read it herePDF

We give a detailed conformal-flow proof of the numerical Riemannian Penrose inequality in every dimension n ≥ 3 for complete asymptotically flat exteriors with nonnegative scalar curvature and full compact frontiers that are outer minimizing and locally perimeter minimizing. The metric extends smoothly through the possibly singular frontier; neither spin nor frontier connectedness is assumed. The proof follows the conformal-flow approach of Bray, Bray–Lee, and Bi–Zhu.

Equality and rigidity in the spacetime Penrose inequality

27 September 2026, current edition.

Read it herePDF

Equality in the spacetime Penrose inequality identifies the original initial data as a spacelike slice of a Schwarzschild–Tangherlini exterior, smoothly attached to its horizon, under the stated outermostness and decay hypotheses. We prove this in every spatial dimension n ≥ 3 for a strong-decay exterior class and for weaker decay in dimensions three and four. In dimension three the finite-component theorem forces a single spherical horizon and gives qualitative strictness for disconnected boundaries.

Boundary graph deformations for the spacetime Penrose inequality

27 September 2026, current edition.

Read it herePDF

We construct graph and conformal deformations of trapped initial-data exteriors in three and four spatial dimensions. The resulting metrics have nonnegative scalar curvature, strictly negative inner mean curvature, a lower bound protecting every enclosing cut, and an arbitrarily small upper error in ADM energy. We also give a direct four-dimensional maximal vacuum construction that retains a noncompact decaying second fundamental form. These constructions give boundary routes to the corresponding numerical Penrose inequalities.

Area-controlled end replacement and the Bondi Penrose inequality in the CKS class

27 September 2026, current edition.

Read it herePDF

We replace a three-dimensional Cha–Khuri–Sakovich hyperboloidal end by an asymptotically flat end while preserving the dominant energy condition and each fixed compact interior. For strictly future-timelike CKS initial-data charge, the replacements lose asymptotically no enclosing area and their ADM masses tend to the invariant Bondi mass. Combining this construction with the companion numerical spacetime Penrose theorem yields the sharp Bondi bound for possibly disconnected weakly future trapped boundaries in this class. Horizon-regular Schwarzschild exteriors attain equality at every positive mass.

One Lean statement in this family

Lean is a language for mathematical statements and proofs that a computer can verify. The Lean statement below is shown beside its possible paper counterpart, with the reason they were linked. The outside readers find that the release’s Lean states a supporting or different result, so the theorem it is paired with is shown under its own heading.

For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.

CKSBondiPenrose

The paper states

Theorem 1.1 (Area-controlled end replacement)

In Area-controlled end replacement and the Bondi Penrose inequality in the CKS class, 27 September 2026

Let (\Omega,g,K) be a smooth connected orientable three-dimensional exterior, complete including its nonempty compact smooth boundary, with exactly one end of class (1.3). Suppose DEC holds and E_B>|P_B|. There is a balanced chart such that, for every sufficiently large R, smooth data (G_R,k_R) on the same exterior have the following properties:

  1. 1.

    They agree with (g,K) on the compact side of r=R and satisfy DEC.

  2. 2.

    For numbers 0\leq\varepsilon_R<1 with \varepsilon_R\to0, G_R\geq(1-\varepsilon_R)g everywhere on \Omega.

  3. 3.

    The end is asymptotically flat, with G_R-\delta=O_j(r^{-1}) for every fixed finite j, and k_R=0 sufficiently far out. The constraints are integrable and its charges satisfy P_R=0, E_R=m_B+\eta_R, where 0\leq\eta_R\leq2R^{-1/2}.

The new exterior is complete and A_{\min,G_R}(S)\geq(1-\varepsilon_R)A_{\min,g}(S). No condition on the boundary expansion is needed.

The words they share: area, asymptotically, boundary, compact, condition, connected, controlled, data, dimensional, exterior, fixed, flat, replacement.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Area-controlled end replacement and Schwarzschild equality examples

CKSBondiPenrose.lean, the release lists it as a supporting statement.

theorem area_controlled_end_replacement    (g : OAI.CKSMetricGluing.SmoothMetric OAI.CKSGeometricCuts.I3 (M := N)) (K : OAI.CKSMetricGluing.InnerField OAI.CKSGeometricCuts.I3 (M := N))    (hK : ContMDiff OAI.CKSGeometricCuts.I3 (OAI.CKSGeometricCuts.I3.prod 𝓘(ℝ,OAI.CKSLorentz.SpatialBilinear)) ∞ (OAI.CKSMetricGluing.innerSection OAI.CKSGeometricCuts.I3 K))    (hKsym : ∀ x v w, K x v w = K x w v)    (hOrient : OAI.CKSSourceExterior.Orientable (N := N))    (hScompact : IsCompact (OAI.CKSGeometricCuts.I3.boundary N)) (hSnonempty : (OAI.CKSGeometricCuts.I3.boundary N).Nonempty)    (hcomplete : OAI.CKSReplacementCompleteness.IsComplete OAI.CKSGeometricCuts.I3 g.toContinuousRiemannianMetric)    (hDEC : OAI.CKSSpatialManifold.PhysicalDEC OAI.CKSGeometricCuts.I3 g.inner K)    (d : OAI.CKSSourceExterior.CKSData g K)    (ht : ‖(OAI.CKSLorentz.bondiCharge d.massAspect).2‖ < (OAI.CKSLorentz.bondiCharge d.massAspect).1) :    ∃ (d' : OAI.CKSSourceExterior.CKSData g K) (R₀ : ℝ) (ε : ℝ → ℝ),      OAI.CKSLorentz.bondiCharge d'.massAspect =        (Real.sqrt ((OAI.CKSLorentz.bondiCharge d.massAspect).1^2 - ‖(OAI.CKSLorentz.bondiCharge d.massAspect).2‖^2),0) ∧      d'.chart.radius < R₀ ∧ 12 ≤ R₀ ∧ Tendsto ε atTop (𝓝 0) ∧      OAI.CKSFullCutArea.minEnclosingArea g < ⊤ ∧      ∀ R ≥ R₀, (0 ≤ ε R ∧ ε R < 1) ∧

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

The file states one more theorem: schwarzschild_equality_examples.

two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.

Read the complete Lean statement

Independent comparisons and proof-verification reports

Does the Lean express the advertised result?

Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.

MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.

MathVet finds that the Lean statements express a supporting result (their term: “supporting-only”).

Their note: The two challenge theorems are CKSSourceExterior.area_controlled_end_replacement (a 3-dimensional Cha-Khuri-Sakovich hyperboloidal end can be replaced by asymptotically flat ends keeping the compact interior, completeness and DEC, with Tendsto (spatialADMEnergy G)... (√(m² - |p|²) + η) and ε R → 0 area loss) and schwarzschild_equality_examples (m) (hm : 0 < m) (the Schwarzschild data satisfy MainHypotheses, bondiMass d = m, minimumEnclosingArea g = 16π m²). Neither states the Penrose inequality: the summary’s headline (invariant ADM mass ≥ √(min enclosing area/16π) for asymptotically flat data in every dimension n >= 3 under DEC/weak future trapping, with equality rigidity and charged bounds) is absent; docs: ‘The paper’s general Bondi-Penrose inequality... remains unformalized’ and the conditional inequality ‘is not selected’. The challenge deals with the dimension-3 Bondi/CKS class only.

Definitions the group asks readers to compare with the paper: Entire geometric-analysis stack is hand-built inside one 3.6k-line challenge file (MetricJet, TensorJet, PhysicalDEC, CKSData, minimumEnclosingArea, bondiCharge, spatialADMEnergy,...) on top of Mathlib manifolds; none is a Mathlib notion and the file has dozens of auxiliary definitions.

“supporting-only”, in their words: The challenge statements state a lemma or auxiliary result, not the headline.

Their method: An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.

cert-machine finds that the Lean statements express a different result (their term: “DIFFERENT”).

The gap they name: The entire headline. No Penrose inequality of any kind is stated (neither the headline’s ADM / asymptotically-flat enclosing-area inequality in any dimension n >= 3, nor even the CKS paper’s Bondi-mass inequality), no equality rigidity, no charged dyonic three-dimensional upper-area bound, no higher-dimensional purely electric extension. What is stated is a three-dimensional CKS-class end-replacement construction (from one of the family’s 13 manuscripts) and Schwarzschild sharpness examples for an inequality that is itself not stated. The union neither implies the headline nor is implied by it.

“DIFFERENT”, in their words: The challenge statements state a different theorem from the headline.

Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.

OpenAI’s own note on what its Lean covers

The formalization replaces a three-dimensional Cha–Khuri–Sakovich hyperboloidal end by asymptotically flat ends while preserving each fixed compact interior, completeness, and the dominant energy condition. For strictly future-timelike initial-data charge, the ADM masses approach the invariant Bondi mass and the loss of enclosing area tends to zero.

The Comparator also includes canonical Schwarzschild equality examples at every positive mass, with $m_{\mathrm{Bondi}}=m$ and enclosing area $16\pi m^2$. The paper’s general Bondi–Penrose inequality for possibly disconnected weakly trapped boundaries remains unformalized. The implementation retains a conditional inequality for the connected marginal-boundary case, assuming the asymptotically flat exterior Penrose inequality. This supporting result is not selected as a substitute for the paper’s main inequality.

AI-drafted comparisons, with no recorded human review

  • Area-controlled end replacement and Schwarzschild equality examples CKSBondiPenrose

    Unreviewed AI draft: states a paper’s theorem as the paper does. States the paper’s end-replacement theorem (asymptotically flat ends replacing a hyperboloidal end, with masses approaching the Bondi mass and enclosing-area loss tending to zero) and Schwarzschild equality examples. The Bondi–Penrose inequality, which the note calls the paper’s main inequality, is outside this statement.

Who ran the proof-verification program?

These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.

These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.

Area-controlled end replacement and Schwarzschild equality examples CKSBondiPenrose

Two reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal report
cert-machine“CERTIFIED”Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.10 October 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.8 October 2026Original report

Explanations by others

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

  • seaworld008, seaworld008/openai-math-top30: thirty selected families explained in Chinese, 7 October 2026. Source

    Chinese-language explainer for general readers, with a beginner’s section, a specialist section, background on why the problem was hard and a diagram; it ends by saying it paraphrases OpenAI’s summary and does not represent consensus.

  • 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.

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 explanationCompare the Lean statement with the paperSuggest a source attributionSuggest 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

  • Robert Joseph George, Do the Lean statements in openai/math match their papers?, 7 October 2026. Source

    The headline claims the sharp spacetime Penrose inequality for every dimension from three, but only a three-dimensional end replacement is formalised.

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.

Read the Lean statement against the paper

  • An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded. Open the form

Identify the theorem the catalogue describes

  • Family 260 No single paper statement clearly matches OpenAI’s description by wording, and no review identifying the intended theorem is recorded. Open the form

Address a question raised in an independent assessment

Compare the proposed paper and Lean matches

  • Family 260 Atlas records no review of whether each linked Lean statement and paper theorem mean the same thing. Open the form