[cadamcat]

Renumbered: since #5135 this problem is JSP-001067 (it was JSP-001068 when this PR was opened). I updated the title and the IDs below; the pinned catalog links still point to the version before the renumbering.

Submission type

• Mathematical solver information
• Lean proof or formalization author information

A complete Lean formalization of the stated problem. The mathematics is OpenAI's, already recorded in the catalog; I claim only the Lean formalization.

Problem

• Problem ID(s): JSP-001067
• Original problem source and exact location (page, section or problem number): JSP-001068 at that commit, now JSP-001067, problems/catalog-1001-1022.md, lines 1596–1619 at awards commit fd8fa66abb4e21df828fdebc25298e9ad75521bd: "For the full nonrelativistic Coulomb model with two electron spin states, are the first ionization energy and the radius containing all but an expected half-electron of a neutral atom bounded above and below by positive universal constants, and does the generalized removal energy I_m(Z) have Thomas-Fermi asymptotics I_m(Z)/m^(7/3) -> a_TF when m -> infinity and Z/m -> infinity?"
• Current entry and proposed change:
  • Lean proof: No becomes Yes, linking the proof, with Formalization contributors: Yao Xu (@cadamcat). OpenAI's two Lean libraries, which the proof builds on, stay linked and credited in the same cell.
  • Attribution basis: one sentence added for the Lean credit.
  • The diff is confined to the JSP-001067 detail table (2 lines). Eligible to claim, the review notes (which describe OpenAI's narrower formalization) and the index in problems/README.md are left for maintainers.
• Related issue, if any: none.
• Related PRs and how this contribution differs: I searched PRs and issues on 2026-10-14 for "JSP-001068" and for "ionization". The only hit is #5049, which added the record with Lean proof No. To my knowledge, this is the first submission of a Lean proof of the full stated problem.
• Scope. The 2026-10-13 source review lists what OpenAI's Lean targets do not supply: the two-sided first-ionization bound, the two-sided half-electron radius bound at finite Z, a separate existence result for ground states, and fixed-m convergence. This formalization proves the first three. Fixed-m convergence is not part of the problem description, which asks for the limit as m → ∞ and Z/m → ∞ jointly, and OpenAI's paper does not assert it (Generalized ionization energies, Theorem 1.1: "No convergence of I_m(Z) at a fixed m is asserted or assumed"). The classical excess-charge bound (Theorem 1.1 of Uniform excess charge) is also outside the description and not formalized.
• For solver/publication updates: not applicable; the catalog already records the publications and OpenAI as solver.

Formal statement

• Complete mathematical solution (provided earlier or in this PR): public proof or publication, relevant theorem/pages, version or date: provided earlier in the catalog record. The proof follows OpenAI, Uniform excess charge for Coulomb molecules and the outer radius of neutral atoms (Theorem 1.2, Corollary 1.3, Lemma 2.5), and Generalized ionization energies for full Coulomb atoms (Theorem 1.1), OpenAI Math Release preprints of September 24, 2026 (openai/math at 1581d4cbdd69a0faf34b2089614fe2a814316a6a).

• Mathematical review reference or current review status: the papers are unrefereed preprints; the catalog records "independent mathematical review pending".

• Formal statement location, pinned to a full commit SHA: AtomicIonization/Challenge.lean, commit d083b8d861d96980b154be3945696e9d277e53c2.

• Fully qualified target theorem name: AtomicIonization.main_theorem : AtomicIonization.Statement

• Statement origin (maintainer-approved reference and version, or proposed statement requiring review): proposed statement requiring review. The model is copied verbatim from OpenAI's Comparator challenge CoulombRadii.lean (form domain, energy form, normalized ground states, spin-summed density, exterior mass), and the Thomas–Fermi coefficient's characterization verbatim from CoulombIonization.lean. The sector energy, the ionization energies and the half-electron radius are defined in Challenge.lean.

• Correspondence to the original problem: definitions, assumptions, quantifiers, conclusion and all required cases; explain any differences from an approved statement:

  def Statement : Prop :=
    (∃ c C : ℝ, 0 < c ∧ c ≤ C ∧ ∀ Z : ℕ, 1 ≤ Z →
        c ≤ ionizationEnergy 1 Z ∧ ionizationEnergy 1 Z ≤ C) ∧
    (∀ N : ℕ, ∃ ψ : Wavefunction (N + 1), IsNormalizedGroundState (N + 1) ψ) ∧
    (∃ c C : ℝ, 0 < c ∧ c ≤ C ∧ ∀ N : ℕ, ∀ ψ : Wavefunction (N + 1),
        IsNormalizedGroundState (N + 1) ψ → c ≤ halfRadius ψ ∧ halfRadius ψ ≤ C) ∧
    (∃ a : ℝ, 0 < a ∧ TFCharacterization a ∧
      ∀ m Z : ℕ → ℕ, (∀ j, 1 ≤ m j ∧ m j < Z j) →
        Tendsto m atTop atTop →
        Tendsto (fun j => (Z j : ℝ) / (m j : ℝ)) atTop atTop →
        Tendsto (fun j => ionizationEnergy (m j) (Z j) / (m j : ℝ) ^ (7 / 3 : ℝ))
          atTop (𝓝 a))

  • Model. One nucleus of integer charge Z at the origin, n electrons with two spin states, kinetic term -Δ/2, wavefunctions antisymmetric in the joint space–spin variables, the Hamiltonian taken through its quadratic form on the antisymmetric H¹ form domain. These are the conventions of Uniform excess charge §1.1 and of OpenAI's challenges.
  • Energies. groundEnergy Z n is the infimum of the energy over normalized vectors of the form domain, with groundEnergy Z 0 = 0; ionizationEnergy m Z = groundEnergy Z (Z - m) - groundEnergy Z Z is the paper's I_m(Z) = E_Z(Z-m) - E_Z(Z). The infimum is taken in ℝ, where an unbounded set would give 0; the repository proves that it equals OpenAI's form bottom (package groundEnergy_eq_formBottom), so the defined value is the true ground-state energy. Z - m is truncated subtraction, used only with m ≤ Z.
  • Clause 1 is Corollary 1.3: two-sided universal bounds on I₁(Z) for every integer Z ≥ 1.
  • Clauses 2–3 are Lemma 2.5 (existence) and Theorem 1.2 (bounds). The neutral atom is indexed by Z = N + 1 ≥ 1; the bounds hold for every normalized ground state, as in Theorem 1.2. halfRadius ψ = sInf {r ≥ 0 | exteriorMass ψ r ≤ 1/2} is the paper's R(Ψ_Z) (its equation (1.2)).
  • Clause 4 is Theorem 1.1 of Generalized ionization energies: the joint limit over every pair of sequences of integers with 1 ≤ m_j < Z_j, m_j → ∞ and Z_j/m_j → ∞, which is the sequential form of the limit in the description. TFCharacterization a says I_m^TF(Z) → a·m^{7/3} as Z → ∞ for every real m > 0; it determines a uniquely, so a is the Thomas–Fermi constant a_TF, and 0 < a is asserted.
  • Challenge.lean imports Mathlib alone and has no hypotheses.

Proof submission

[
  {
    "repository": "https://github.com/cadamcat/atomic-ionization-lean4",
    "branch": "main",
    "commit": "d083b8d861d96980b154be3945696e9d277e53c2"
  }
]

• Proof file at the selected commit and fully qualified theorem name: AtomicIonization/Main.lean, AtomicIonization.main_theorem.
• How the proof establishes the formal statement above, including any separate verification entry:
  • AtomicIonization.main_theorem is AtomicIonization.Blueprint.main (Blueprint/Main.lean), which derives Statement from ten package theorems stated in Blueprint/Interfaces.lean and proved in their own directories. The README maps each package to the paper (Lemma 2.5, Propositions 12.3, 13.1 and 14.1, §§12 and 14 of Uniform excess charge).
  • Clause 4 is transported from OpenAI's OAI.CoulombAtom.generalized_ionization through a proved bridge between the copied model and OpenAI's library (package joint_limit).
  • OpenAI's CoulombRadii and CoulombIonization directories are included unchanged under OAI/ (Apache-2.0, THIRD_PARTY.md), so the build needs only Mathlib.
• Selected commit and branch: d083b8d861d96980b154be3945696e9d277e53c2 is the annotated tag v1.0.0, and the repository was published as that single commit. One later commit on main, bc31d2968fc791f92e6647eb45b202cd22b6df86, adds the verification record docs/verification.md and a README pointer; it changes no Lean file.
• No placeholder proof: scripts/verify.sh builds the library and fails if the final theorem or any package theorem depends on sorryAx or an axiom other than propext, Classical.choice and Quot.sound. No proof in the repository uses sorry, admit or an added axiom.
• Public history of the selected commit: the repository was created 2026-10-14T14:09:00Z (created_at). The activity feed records the creation of refs/heads/main at d083b8d861d96980b154be3945696e9d277e53c2 at 2026-10-14T14:09:11Z. Git commit and tag dates are author-set metadata.
• Software Heritage: save request 2556889, full visit at 2026-10-14T14:09:20Z, snapshot swh:1:snp:7995b037bb25ad854e5b54b223e3200f69aeaba6.

Reproduction

• Exact Lean version and lean-toolchain path: leanprover/lean4:v4.34.1, in lean-toolchain.

• Pinned dependencies (including mathlib, if used) and manifest path: Mathlib at commit d13f23b723b8a846827a245b89c10fc7d3f11612, required in lakefile.lean; all revisions are fixed in lake-manifest.json. OpenAI's code is vendored, not a dependency.

• Build instructions pinned to the selected commit: README.md.

• Commands for setup, clean build and checking each target theorem; include a separate statement-to-proof check if needed:

  git clone https://github.com/cadamcat/atomic-ionization-lean4 && cd atomic-ionization-lean4
  git checkout d083b8d861d96980b154be3945696e9d277e53c2
  lake exe cache get
  ./scripts/verify.sh                 # build, axioms of the final theorem and of every package theorem
  lake env leanchecker --fresh AtomicIonization.Main

• Axiom audit command and output for each target (for example, #print axioms Fully.Qualified.theoremName): run by scripts/verify.sh through Verification/Axioms.lean:

  'AtomicIonization.main_theorem' depends on axioms: [propext, Classical.choice, Quot.sound]
  

Pre-submission Lean verification (optional)

• Method/tool and version, if available: my own procedure; the lean-verify skill was not used. I made a fresh clone of the selected tag into an empty directory, ran the commands above at 12 threads, and then ran Comparator.

• Checked repository and full commit SHA; identify any difference from the submitted version: d083b8d861d96980b154be3945696e9d277e53c2, the submitted commit.

• Verification date, actual conclusion and limitations: 2026-10-14, 14:10 to 14:51 UTC; recorded in docs/verification.md.

  Step	Result
  lake exe cache get, lake build	exit 0, 9978 jobs; OpenAI's vendored modules built from source
  #print axioms AtomicIonization.main_theorem	propext, Classical.choice, Quot.sound; the same for every package theorem
  lake env leanchecker --fresh AtomicIonization.Main	exit 0
  Comparator ca04cfc7, lean4export 076e8e57, nanoda_lib 3a240721, enable_nanoda true, definition_names empty	exit 0; nanoda and Lean's kernel both accepted the theorem
  Comparator control: half-electron threshold in the challenge changed from 1 / 2 to 1 / 3	rejected ("Const does not match between challenge and target 'AtomicIonization.Statement'")
  nanoda control	accepted a correct proof; rejected a sorry proof and a tampered numeral

  Limitations:

  • Comparator ran with its development fake-landrun.sh, not the Landrun sandbox.
  • Mathlib came from its official cache.
  • The author ran the check; no independent person has reviewed the formalization.

• Summary of statement correspondence, coverage, Lean checks and trust dependencies: correspondence is in the Formal statement section. Trust: the Lean kernel, compiler and core library, Mathlib, and OpenAI's two vendored libraries.

• Report in this PR or external report/log/evidence links, if available: in this PR and in docs/verification.md.

Attribution

• Mathematical solver(s) and contribution, if applicable: OpenAI, as recorded in the catalog. I am not an author of the papers.
• Lean formalization author(s) and contribution, if applicable: Yao Xu (@cadamcat), the author of the formalization in AtomicIonization/: the statement, the bridge to OpenAI's library, and the proofs of the ionization bounds, ground-state existence and radius bounds. OpenAI's Lean libraries supply the many-electron form domain, the spectral and variational theory of the atom and the generalized-ionization asymptotics; they are included unchanged and credited in THIRD_PARTY.md.
• Independent verifier(s), if any: none.
• Public authorship evidence: the repository is owned by my account, cadamcat. AUTHORS.md at the selected commit names Yao Xu as author of the formalization and the papers as the work of OpenAI. The public history has one author.
• The Lean formalization and this PR were prepared by the author with AI assistance; all proofs are verified by the Lean 4 kernel.

Submission checklist

• I changed only the relevant catalog's solver attribution, Lean proof information or supporting sources and supplied the applicable evidence.
• The submitted result fully solves the original problem. Any submitted Lean proof is complete at the specified commit, with no sorry, admit or added unproved assumptions replacing proof steps.
• For Lean: I have linked the complete mathematical solution and its proof or publication evidence provided earlier, or supplied them in this PR, and identified the mathematical solver and Lean formalization author separately.
• For Lean: I am claiming my own contribution in the original personal or organization repository, with verifiable contribution evidence for an organization repository; the selected commit is in the named branch, and I supplied statement correspondence, reproduction commands and axiom audit results.
• This PR contains no Lean source files, archives, binaries, vendored dependencies or private identity/contact/payment information.