How many electrons can an atom hold?
Three AI preprints claim the ionization conjecture for the full Schrödinger model, and Solovej’s generalized version
Covers result 263 in OpenAI’s catalog: all 3 papers. See its connections to other results and the work it cites.
3:50. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
A nucleus of charge Z attracts Z electrons and becomes neutral; in nature, at most one more ever sticks. Hydrogen can hold a second electron, but only because of correlation. Real atoms are remarkably uniform: the tabulated first ionization energies of the first 108 elements stay between about 4 electron volts, for caesium, and about 25, for helium, with no growth as atoms get heavier (our reading of the NIST database).
Mathematically, this was a famous open problem. Barry Simon’s 2000 list asked to prove that the number of electrons an atom can bind, minus Z, stays bounded. Earlier proofs allowed far more: Lieb in 1984, fewer than 2Z plus the number of nuclei; Nam in 2012, about 1.22 Z. In 2025 Lewin wrote that no proof existed even with a constant like 10¹⁰⁰. Solovej proved the bounded version in 2003 for Hartree–Fock theory, an approximation.
Result 263 is three OpenAI preprints, 134 pages, dated September 24, 2026. The main paper, 84 pages, claims that in the full nonrelativistic Schrödinger model, with fermions of two spin states and fixed nuclei of charge at least one, a molecule of total nuclear charge Z strictly binds at most Z + C × (number of nuclei) electrons, with C universal. It also claims the first ionization energies of neutral atoms are bounded above and below by universal positive constants. Two companions claim Solovej’s generalized ionization conjecture: the energy to remove m electrons follows the Thomas–Fermi law, a constant times m^(7/3), as m and Z/m grow, and the outer radii follow the matching Thomas–Fermi law.
What it doesn’t claim
The sharp bound of one or two extra electrons; any explicit value of C, which comes from an argument by contradiction; bosons, where the statement is false; relativity; or the limit of the first ionization energy.
Where it stands
- Posted as preprints
- OpenAI, three papers, 84, 33 and 17 pages, dated September 24, 2026
- Peer reviewed
- Not yet
- Formalized in Lean
- In part: the two asymptotic theorems (docs)
Last checked October 19, 2026. The preprints have not been revised. Lean formalizes the two asymptotic theorems, about 95,000 and 77,000 lines with no unproved steps, which we did not build. The headline theorems of the main paper, bounded excess and the ionization-energy bounds, are not formalized. OSVerify has not reviewed them, and we found no specialist comment.
How the proofs go
- Solovej’s architecture. Compare the true atom with a screened Thomas–Fermi model at every scale, from the nucleus out, and show that the outermost electrons see an almost neutral core.
- The full problem. The new work makes each comparison hold for the full many-body Schrödinger problem, where electrons are correlated, and runs the whole argument by contradiction. That is why C is never computed.
The numbers in the video
- Ours: in a two-electron toy, the state with both electrons alike does not bind hydrogen’s second electron, while letting one electron sit far out does.
- Ours: the limiting constant the papers define but do not compute is about 1.29 electron volts per unit of m^(7/3). For heavy atoms, removing eight electrons costs about 2.5 times the limiting law, so real atoms are far from that regime.
Read the source
- Uniform Excess Charge for Coulomb Molecules and the Outer Radius of Neutral Atoms (PDF), 84 pages.
- Generalized Ionization Energies for Full Coulomb Atoms (PDF), 33 pages.
- Generalized Outer-Electron Radii of Neutral Coulomb Atoms (PDF), 17 pages.
- The Lean formalization notes.
- The collection’s catalog, where this is result 263.
The 3 papers in this result
OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.
Transcript
Read the full script
0:00The question
How many electrons can an atom hold? A nucleus of charge Z attracts Z electrons and becomes neutral; in nature, at most one more ever sticks. Hydrogen can hold a second electron, but only because of correlation: in our two-electron toy, the state with both electrons alike does not bind, while letting one electron sit far out does. Real atoms are remarkably uniform. Our computer read the tabulated first ionization energies of the first 108 elements from the NIST database: they stay between about 4 electron volts, for caesium, and about 25, for helium, with no growth as atoms get heavier. Mathematically, this was a famous open problem. Barry Simon’s 2000 list asked to prove that the number of electrons an atom can bind, minus Z, stays bounded. Earlier proofs allowed far more: Lieb in 1984, fewer than 2Z plus the number of nuclei; Nam in 2012, about 1.22 Z. In 2025, Lewin wrote that no proof existed even with a constant like 10¹⁰⁰. Solovej proved the bounded version in 2003 for Hartree-Fock theory, an approximation.
1:15The claims
Result 263 is three OpenAI preprints, 134 pages, dated September 24, 2026. The main paper, 84 pages, claims that for the full nonrelativistic Schrödinger model, with fermions of two spin states and fixed nuclei of charge at least one, a molecule of total nuclear charge Z strictly binds at most Z plus C times the number of nuclei electrons, with C universal. It also claims first ionization energies of neutral atoms are bounded above and below by universal positive constants. Two companions claim Solovej’s generalized ionization conjecture: the energy to remove m electrons follows the Thomas–Fermi law, a constant times m^(7/3), as m and Z/m grow, and the outer radii follow the matching Thomas–Fermi law. Not claimed: the sharp bound of one or two extra electrons; any explicit value of C, which comes from an argument by contradiction; bosons, where the statement is false; relativity; or the limit of the first ionization energy. Our computer evaluates the limiting constant the papers define but do not compute: about 1.29 electron volts per unit of m^(7/3). Real atoms are far from that regime: for heavy atoms, removing eight electrons costs about 2.5 times the limiting law.
2:44How the proofs go
The architecture follows Solovej’s Hartree-Fock proof: compare the true atom with a screened Thomas–Fermi model at every scale, from the nucleus out, and show the outermost electrons see an almost neutral core. The new work makes each comparison hold for the full many-body Schrödinger problem, where electrons are correlated, and runs the whole argument by contradiction.
3:08Where it stands
The preprints are unrefereed and unchanged since release. Lean formalizes the two asymptotic theorems, about 95,000 and 77,000 lines with no unproved steps, which we did not build; the headline theorems, bounded excess and the ionization-energy bounds, are not formalized. OSVerify has not reviewed them, and we found no specialist comment. If they hold, in the Schrödinger model a neutral atom can bind only a bounded number of extra electrons, however heavy it is, and its outermost electron is held with a strength that never grows without bound or fades to nothing.
Spot a mistake?
This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.