The ionization and generalized ionization conjectures
OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:
For the full nonrelativistic Coulomb model with two electron spin states, proves that a molecule with M fixed nuclei of charges at least one and total charge Z strictly binds at most \(Z+CM\) electrons. Neutral-atom first ionization energies and radii containing all but an expected half-electron have universal positive upper and lower bounds. The energy cost of removing m electrons has Thomas–Fermi asymptotics as \(m\to\infty\) and \(Z/m\to\infty\); neutral-atom outer radii have the corresponding iterated-limit asymptotics, taking \(Z\to\infty\) first. (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 only part of the result described above, or a narrower statement.Read the assessments
The paper’s main theorem is shown as a possible match to OpenAI’s description. No review confirming the selection is recorded.
There is a universal finite constant C such that every nuclear system specified above and every integer n\ge1 satisfy
E_n<E_{n-1}\quad\Longrightarrow\quad n\le Z+CM.
Moreover, E_n=E_{n-1} whenever n>Z+CM. For one nucleus this gives n\le Z+C under strict binding, for every real Z\ge1. The same constant is independent of all charges and nuclear positions.
No Lean statement in the release is paired with this theorem.
Possible match to OpenAI’s description, selected because it shares the most wording. No review confirming the selection is recorded.
For the full nonrelativistic Coulomb atom specified above, with integer nuclear charge Z\ge1, one-electron kinetic term -\Delta/2, and two electron spin states, write E_Z(n)=E(n,Z). There are universal constants 0<c\le C<\infty such that the first ionization energy of the neutral atom satisfies
c\le I_1(Z):=E_Z(Z-1)-E_Z(Z)\le C
\qquad\text{for every integer }Z\ge1.
No Lean statement in the release is paired with this theorem.
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.
Four more possible matches
Theorem 1.1(Generalized ionization energy)in Generalized ionization energies for full Coulomb atoms, 24 September 2026.
Theorem 1.2(Deficit at a prescribed price)in Generalized ionization energies for full Coulomb atoms, 24 September 2026.
Theorem 1.1(Generalized ionization conjecture: radii)in Generalized outer-electron radii of neutral Coulomb atoms, 24 September 2026.
Theorem 1.2(Uniform outer half-electron radius)in Uniform excess charge for Coulomb molecules and the outer radius of neutral atoms, 24 September 2026.
Reported proof verification
Two Lean statements in the release; independent groups report that Comparator accepted runs for all these files at the version shown here.
We prove that a molecule with M fixed nuclei of real charges at least one and total nuclear charge Z strictly binds at most \(Z+CM\) electrons, where C is universal. The result holds for the full nonrelativistic Coulomb Hamiltonian with two spin states and arbitrary distinct nuclear positions. For neutral atoms with integer nuclear charge Z ≥ 1, the first ionization energy and, for every ground state, the radius outside which one half of an electron remains are each bounded above and below by positive universal constants.
We prove the energy part of the generalized ionization conjecture for full nonrelativistic Coulomb atoms with two electron spin states. The energy needed to remove m electrons is asymptotic to \(a_{\mathrm{TF}}m^{7/3}\) whenever \(m\to\infty\) and \(Z/m\to\infty\), with the Thomas–Fermi constant in atomic units. We also obtain both conjectured iterated limits.
We prove the radius part of the generalized ionization conjecture for neutral nonrelativistic Coulomb atoms with two spin states. For every choice of ground states, the upper and lower large-nuclear-charge limits of the radius defined by an expected exterior electron mass m are both asymptotic to \((81\pi^2/2)^{1/3}m^{-1/3}\) as m tends to infinity.
Two Lean statements in this family
Choose one to see it beside the paper theorem it is paired with.
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.
CoulombIonization.lean, the release lists it as a main result.
defMainStatement : Prop := ∃ a : ℝ, 0 < a ∧ TFCharacterization a ∧ JointLimit a ∧ IteratedLimits a⋮theoremgeneralized_ionization : MainStatement := bysorry
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.
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.
Other mathematical statements in OpenAI’s Lean library
Atlas found these propositions by scanning the text of the project’s Model.lean file. Each name links to its definition, with any associated statement file beside it. This list does not record running Lean to interpret or verify those definitions.
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 part of the advertised result (their term: “partial”).
Their note:PRIMARY CLAIM NOT STATED (only a secondary result is formalized). Stated: CoulombIonization.generalized_ionization : ∃ a > 0, TFCharacterization a ∧ JointLimit a ∧ IteratedLimits a (I_m(Z)/m^{7/3} → a_TF as m → ∞ and Z/m → ∞, and the Z → ∞ first iterated limsup/liminf; energies are infima of the full antisymmetric two-spin form with FormAdmissible) and CoulombRadii.generalized_outer_radii (m^{1/3} R_m → (81π²/2)^{1/3} for both limsup and liminf over any sequence of normalized ground states). Not stated: the summary’s first claim, a molecule with M nuclei and total charge Z strictly binds at most Z + CM electrons, and the universal positive upper and lower bounds on first ionization energies/half-electron radii (docs: only ‘large-ionization asymptotics’).
Definitions the group asks readers to compare with the paper:Custom ‘energy’: energy Z N := if N = 0 then 0 else sInf {e | ∃ ψ : FormVector N, FormAdmissible ψ ∧ formEnergy Z ψ = e} (a real sInf, junk 0 if unbounded below, which atoms are not) and IteratedLimits uses real-valued limsup/liminf of ionization m (junk 0 if unbounded); CoulombRadii instead uses EReal-valued limsup/liminf and takes the ground states Ψ N as hypotheses (IsNormalizedGroundState), so it is vacuous if such minimizers did not exist (they do for neutral atoms). TF functional constant tfKinetic = (3/10)(3π²)^(2/3) written by hand.
“partial”, in their words: Only a special case is stated, or a co-equal headline claim has no challenge statement.
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 narrower statement than the advertised result (their term: “NARROWER — UNLINKED”).
The gap they name:Not stated: the uniform excess-charge bound Z + CM for molecules, and the universal two-sided bounds on neutral-atom first ionization energies and half-electron radii. These are the family’s first manuscript, which contains the ionization conjecture of the family title.
“NARROWER — UNLINKED”, in their words: The challenge statements state less than the headline; the missing part comes from a paper the Lean note does not link.
Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.
The formalization gives the large-ionization asymptotics for the full nonrelativistic two-spin Coulomb atom. Let $I_m(Z)$ be the energy needed to remove $m$ electrons from a neutral atom of nuclear charge $Z$. There is a positive coefficient $a_{\mathrm{TF}}$ with the Thomas–Fermi variational characterization such that $I_m(Z)/m^{7/3}\to a_{\mathrm{TF}}$ whenever $m\to\infty$ and $Z/m\to\infty$, with integers $Z>m\ge1$. The corresponding iterated limsup and liminf limits hold with $Z\to\infty$ first. The energy uses the full antisymmetric Sobolev form domain; fixed-$m$ convergence and ground-state attainment are outside this statement.
For neutral Coulomb atoms with two electron spin states, the formalization proves the asymptotic law for generalized outer-electron radii defined by an expected exterior electron mass $m$. For every choice of normalized ground states, both the upper and lower large-nuclear-charge radius limits satisfy
$m^{1/3}R_m\longrightarrow (81\pi^2/2)^{1/3}$ as $m\to\infty$. The large-nuclear-charge limit is taken first. Ground states are inputs to the statement; their existence is not asserted separately.
AI-drafted comparisons, with no recorded human review
Unreviewed AI draft: states a paper’s theorem as the paper does. States the paper’s generalised ionisation theorem: I_m(Z)/m^{7/3} → a_TF as m → ∞ with Z/m → ∞. The deficit theorem and ground-state attainment are not part of the statement.
Asymptotic outer-electron radii of neutral atomsCoulombRadii
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem of the radii paper: m^{1/3}R_m → (81π²/2)^{1/3} for every choice of normalised neutral ground states, with the nuclear-charge limit first.
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.
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.
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.
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.
Robert Joseph George, Do the Lean statements in openai/math match their papers?, 7 October 2026. Source
The headline claims the ionization conjecture and universal bounds, but only asymptotic laws are 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
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 263The 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
Address a question raised in an independent assessment
Only a special case is stated, or a co-equal headline claim has no challenge statement.
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. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.
The challenge statements state less than the headline; the missing part comes from a paper the Lean note does not link.
Their method
Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners…
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
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.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
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.