Equality of the quantum Jellium and uniform electron gas energies
Lieb and Narnhofer (1975) defined the ground-state energy per unit volume of Jellium: electrons in a uniform neutralizing background of density , with no constraint on their density. Lewin, Lieb and Seiringer defined the energy per unit volume of the uniform electron gas: electrons whose density is constrained to equal everywhere, with no background. They called the question of whether the two coincide important for density functional theory, and wrote that the equality is expected in the quantum case. The classical case was proved by Lewin, Lieb and Seiringer and by Cotar and Petrache. Is for every and ?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI co-developed
- Method
- Argument
- Field
- Quantum statistical mechanics
- Posed by
- Lewin, Lieb and Seiringer, Statistical mechanics of the uniform electron gas (J. Ec. polytech. Math. 2018); quantum case expected in The local density approximation in DFT (2020), Sec. 2.2
- Year posed
- 2018
- Years open
- 8y
- Solved
- 2026-10-14
- Model
- ChatGPT (OpenAI) and Claude (Anthropic); versions not stated in the paper
- Vendor
- OpenAI; Anthropic
- Collaborators
- Mihály A. Csirik
- Verification
- Unreviewed
- Publication
- Preprint
- Significance
- 25 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1: for every spin multiplicity , every and every , the canonical Dirichlet Jellium energy of Lieb and Narnhofer equals the Lewin-Lieb-Seiringer UEG energy. Both inequalities are proved. Before this, only was known, and only for a grand-canonical Jellium whose identification with the Lieb-Narnhofer energy had not been proved; the paper proves that inequality for the Lieb-Narnhofer energy too. The upper bound uses packed Dirichlet Jellium balls with compensated shells, not a floating crystal. Consequence: the known UEG properties (high-density expansion, classical limit) transfer to Jellium.
What the AI did
The paper's "Use of AI tools" section: the author "made substantial use of the LLMs ChatGPT (OpenAI) and Claude (Anthropic) in the preparation of this work, including the development of the proofs, writing and making figures", and checked all proofs by hand. The Lean development (folder lean_gpt) was "produced with the help of the same AI tools".
Verification
Read by this site on 3 November 2026, not rebuilt. No independent mathematician has checked the proof yet. Repository xyzw/jellium_ueg, commit 5a2d526 (14 Oct 2026): 75 Lean files, about 14,000 lines, Lean 4.34.0-rc2 with mathlib. A grep for sorry, admit, axiom, native_decide, unsafe, implemented_by, opaque and extern found none. The author's verification.json records a passed run of check.py (warnings as errors, axioms limited to propext, Classical.choice and Quot.sound). The headline Jellium.Main.equality was read: it is relative verification. The two energies are abstract real functions, tied to the physics only through hypothesis structures (LowerPhysical and UpperPhysical StandardLaws, LocalizationLaws) that supply the Lieb-Narnhofer limit, the UEG limit, Lieb-Oxford, stability and localization as inputs; quantum states and operators are interfaces, not constructed. The paper and README say so themselves. No law assumes either comparison. Not Lean-verified: we found no independent anchor for the formal statement (no Formal Conjectures or tracker entry), and it is not a self-contained formalization of the problem. Unreviewed rather than Lean-checked: the formal statement takes the physics inputs as hypotheses, so it does not state the headline on its own.
Sources
Submitted by LucidMarten262 on