oai-math-revised beta

Browse › Mathematical physics › 263 The ionization and generalized ionization conjectures

Generalized outer-electron radii of neutral Coulomb atoms

OpenAI · September 24, 2026

Lean

Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion

Edit NOTES.md · Existing issues · Source on GitHub

Abstract

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.

If the PDF does not display here, open it directly: Open PDF.

Notes

No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.

Automatically collected notes (unreviewed)

work in progress

Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.

Follow-up works

  • muralisubbarao2 (GitHub), TR-M530-Ram-Outer-Electron-Radii (GitHub repository "Improved solutions to 239 of the 722 math problems posted by OpenAI", undated). A technical report whose readable outline and links point to this preprint and its foundation companion; the repository README calls its reports "a first draft prepared with the help of GPT 6 Astra" that has "not been verified by humans yet". [AI-generated per source]

Formalization

  • OpenAI math release, lean/docs/263.md: The ionization and generalized ionization conjectures (Lean scope notes, 6 October 2026). States that the formalization proves $m^{1/3}R_m\to(81\pi^2/2)^{1/3}$ for both the upper and lower large-$Z$ limits, for every choice of normalized neutral ground states, which are supplied as inputs without asserting their existence; the comparator statement is CoulombRadii.lean. [family-level]
  • Yao Xu (cadamcat), atomic-ionization-lean4 (GitHub, Lean 4/Mathlib). A third-party Lean 4 development that bundles OpenAI's CoulombRadii library unchanged; its main statement covers the companion papers' half-electron radius bound and energy asymptotic, not this paper's sharp radius limit. [AI-generated per source] [family-level]

Possibly relevant literature (found by the agent, not checked)

  • P. T. Nam, The ionization problem in quantum mechanics (arXiv:2206.15393, 2022; in the EMS volume for E. H. Lieb's 90th birthday). A survey of the ionization problem, giving background on the radius questions in the generalized ionization conjecture addressed by Theorem 1.1.

Digests and expositions

Elsewhere

Independent sites; their content is not reviewed here.

Cite

@misc{OAI:Generalized-outer-electron-radii-of-neutral-Coulomb-atoms-September-24-2026,
  author = {{OpenAI}},
  title = {{Generalized outer-electron radii of neutral Coulomb atoms}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Generalized-outer-electron-radii-of-neutral-Coulomb-atoms-September-24-2026/paper.pdf}{OAI:Generalized-outer-electron-radii-of-neutral-Coulomb-atoms-September-24-2026}},
  year = {2026}
}

Lean formalization

OpenAI provides Lean files for this family: lean/docs/263.md. The Lean statements have not been checked by people against the paper's claims.

Family 263: The ionization and generalized ionization conjectures

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.

Other papers in this family: