Spacetime Penrose inequalities
The spacetime Penrose inequality (Penrose conjecture for general initial data) bounds the mass of an asymptotically flat initial data set below in terms of the area of its horizon, without assuming time symmetry. Manuscripts dated 5 October 2026 in OpenAI's public mathematics collection (github.com/openai/math) claim sharp versions of it. This page summarizes the published claims and lists publicly available follow-up work.
Background
- According to the introduction of the main manuscript, for time-symmetric data Huisken and Ilmanen proved the connected-horizon inequality by weak inverse mean curvature flow, and Bray proved the total-area bound for possibly disconnected horizons by conformal flow. Bray and Lee extended the numerical Riemannian inequality to spatial dimensions below eight. Bray and Khuri developed a generalized Jang reduction, with spherical existence results and conditional nonspherical constructions. Allen, Bryden, Kazaras and Khuri obtained a universal suboptimal mass–area bound in three dimensions, and Khuri and Kunduri proved the sharp inequality for SU(n+1)-invariant cohomogeneity-one data in spatial dimensions 2(n+1).
The original results
- Claims. The collection's contents list states that family 260 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 stated decay assumptions, with equality rigidity under additional horizon hypotheses, and charged extensions. The abstract of the main manuscript, Spacetime Penrose inequalities: enclosing area, charge, and rigidity, states sharp spacetime Penrose inequalities for invariant ADM mass and minimum enclosing area in three and four spatial dimensions, allowing arbitrary second fundamental form, nonzero momentum, disconnected weakly future trapped boundary and finitely many ends, with equality characterizations by Schwarzschild and Schwarzschild–Tangherlini data, a charged upper-area inequality in three dimensions, and a local Schwarzschild–anti-de Sitter inequality.
- Sources (openai/math repository, commit
1581d4c):- Spacetime Penrose inequalities: enclosing area, charge, and rigidity;
- A Charged Reduction of the Spacetime Penrose Inequality in Spatial Dimensions at Least Four;
- The spacetime Penrose inequality with charge and original-data rigidity;
- The Kerr–Newman Penrose Inequality for Axisymmetric Electrovacuum Exteriors.
- Formalization, as described by the repository. The scope note lean/docs/260.md describes a formalization of an end-replacement construction (a three-dimensional Cha–Khuri–Sakovich hyperboloidal end replaced by asymptotically flat ends) and Schwarzschild equality examples. It states that the paper's general Bondi–Penrose inequality for possibly disconnected weakly trapped boundaries remains unformalized. The Comparator statement is
CKSBondiPenrose.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 16 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family's challenge CKSBondiPenrose "supporting-only" and records a sandboxed Comparator pass. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-15 (listed) | H. Bray, T. Dolmen, M. Khuri, D. Schmidt, Proof of the Penrose Conjecture for Maximally Parameterized Initial Data Sets, arXiv:2610.20559 | Parallel result (special case) and remark | Proves the spacetime Penrose inequality for asymptotically flat initial data sets in all dimensions n ≥ 3 under the dominant energy condition, for data admitting a "maximally parameterized form", in which the second fundamental form is locally parameterized by n(n+1)/2 functions. The proof uses a new one-parameter family of generalized Schoen–Yau identities, a comparison metric with nonnegative scalar curvature and the Riemannian Penrose theorem of Bi and Zhu. The abstract notes that the full conjecture follows whenever a certain system of PDEs can be solved, and states: "Essentially, we believe this is what the OpenAI paper [27] posted last week on October 6, 2026 claims to have done." | arXiv preprint. |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.