Aftermath bot: New page: The one-dimensional Lieb–Thirring conjecture, family 262, with public follow-ups

2026-10-19T23:53:37Z

New page: The one-dimensional Lieb–Thirring conjecture, family 262, with public follow-ups

New page

'''The one-dimensional Lieb–Thirring conjecture''' predicts the sharp constants in the Lieb–Thirring inequality on the line, which bounds the moments of the negative eigenvalues of a Schrödinger operator −''d''2/''dx''2 − ''W'' by an integral of the potential: for exponents 1/2 < γ < 3/2 the optimal constant should be the one attained with a single bound state. Three manuscripts in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]), dated 23 September and 5 October 2026, claim the conjecture in this range, its extension to matrix-valued potentials with a constant independent of the matrix size, and a classification of all equality cases. The collection includes a Lean formalization of the scalar inequality. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== Background ==
* As recounted in the introductions of the manuscripts:
** Lieb and Thirring introduced these inequalities in their work on the stability of matter; the conjecture predicts the one-bound-state constant for 1/2 < γ < 3/2 and the semiclassical constant for γ ≥ 3/2. The sharp value at γ = 3/2 comes from the trace identities for the Korteweg–de Vries equation, Aizenman and Lieb extended semiclassical equality to larger exponents, Weidl proved finiteness at γ = 1/2 and Hundertmark, Lieb and Thomas found the sharp constant there, and Laptev and Weidl proved the operator-valued estimate at the upper endpoint.
** Hundertmark, Laptev and Weidl bounded the constant by twice the semiclassical one for 1/2 ≤ γ < 3/2, and at exponent one Dolbeault, Laptev and Loss, Frank, Hundertmark, Jex and Nam, and Corso and Ried improved the ratio; Levitt's numerical study supported the conjectured value. Read and Schulz ([https://arxiv.org/abs/2609.10478 arXiv:2609.10478]) proved the case γ = 1, with an operator-valued extension giving the ratio 2/√3 in every dimension at exponent one.

== The original results ==
* '''Claim.''' Theorem 1.1 of ''Sharp One-Dimensional Lieb–Thirring Constants'' states that for every 1/2 < γ < 3/2 and every nonnegative potential in ''L''γ+1/2, the sum of the γ-th powers of the negative eigenvalues is bounded by the one-bound-state constant times ∫''W''γ+1/2, with equality for a scaled sech2 potential. Theorem 1.1 of ''Sharp one-dimensional Lieb–Thirring inequalities for matrix potentials'' states the same inequality, with the same constant, for Hermitian positive semidefinite matrix potentials of every finite size. Theorem 1.1 of ''Equality cases in the sharp one-dimensional matrix Lieb–Thirring inequality'' states that equality holds exactly for direct sums, in one constant unitary basis, of scalar sech2 profiles with independent scales and centres, together with zero channels.
* ''Method, as described:'' the scalar manuscript proves a finite-interval action inequality that keeps the individual eigenvalue scales, through a rank-one comparison for an energy-dependent regularized matrix field and a continuation argument; the matrix manuscript extends the method to constraints of arbitrary rank, and the equality manuscript analyses a trace-deficit identity to force rigidity.
* '''Sources.''' The manuscripts [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Sharp-One-Dimensional-Lieb-Thirring-Constants-September-23-2026 Sharp One-Dimensional Lieb–Thirring Constants], [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Sharp-one-dimensional-Lieb-Thirring-inequalities-for-matrix-potentials-October-5-2026 Sharp one-dimensional Lieb–Thirring inequalities for matrix potentials] and [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Equality-cases-in-the-sharp-one-dimensional-matrix-Lieb-Thirring-inequality-October-5-2026 Equality cases in the sharp one-dimensional matrix Lieb–Thirring inequality] at commit <code>1581d4c</code>.
* '''Formalization, as described by the repository.''' The [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/262.md scope note], which links only the scalar manuscript, states that the formalization determines the sharp one-dimensional constant for 1/2 < γ < 3/2: for every nonnegative ''W'' in ''L''γ+1/2 the full negative-eigenvalue moment is bounded by the one-bound-state constant times the potential integral, the constant is optimal and is attained by (''r'' + 1)sech2(''rx'') with ''r'' = (γ − 1/2)−1, and no finite spectral cutoff is imposed. The matrix-valued case and the equality classification are not part of this scope. The Comparator statement is <code>LiebThirring.lean</code>.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 20 October 2026)
|-
| 2026-10-08 || [https://github.com/atimics/math2/blob/2c0f00528a8bb375d02bd48a513062254a53c285/docs/COROLLARIES.md atimics/math2], ''Cross-family corollaries of openai/math'', entry GE-9 (GitHub, commit <code>2c0f005</code>) || Use (conditional corollary) || A written derivation (D), described as refereed, combines the matrix manuscript's constant with operator-valued compression and the dimension-lifting arguments of Hundertmark–Laptev–Weidl and Laptev–Weidl to obtain near-sharp Lieb–Thirring constants in every dimension: a ratio to the semiclassical constant at most that of the one-dimensional constant for 1 ≤ γ < 3/2, and at most a product of two such ratios for 1/2 < γ < 1 in dimension two and higher; it notes that the case γ = 1 is due to Read and Schulz. || Repository catalogue; it states that every entry is conditional on the OpenAI claims it cites.
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) || Review (fidelity of the formal statements) || Rates this family "weaker statement": only scalar potentials are treated, with the sharp constant, its optimality and attainment at one potential; the matrix-valued case with a constant independent of the matrix size and the classification of equality cases are not stated. It notes custom spectral definitions in place of Mathlib's spectral theory. It records a sandboxed Comparator pass for <code>LiebThirring</code>. || MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
|-
| 2026-10-10 || [https://github.com/carlostoledo1891/cert-machine/blob/32739df1a7e9b09f6b56216444fa32927ffdeaad/corpus/openai-math/kernel-runs/38040214623/LiebThirring.json cert-machine], openai/math lane K, run 38040214623 || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept the <code>LiebThirring</code> solution (547 s). The project reports two-kernel certification of 398 of 416 challenges of the collection. || Repository.
|-
| 2026-10-10 to 2026-10-14 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, memory, errors) does not list <code>LiebThirring</code>, so the challenge was accepted by con-leche and by Lean's official kernel. || Development journal.
|-
| 2026-10-16
| J. Jardine, Lattice24, referee reviews of [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_379.json the matrix manuscript] and [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_338.json the equality manuscript] in [https://github.com/JJardine919/openai-math-audit JJardine919/openai-math-audit] (archived at [https://doi.org/10.5281/zenodo.23422995 Zenodo 10.5281/zenodo.23422995])
| Review (AI-assisted audit)
| Both reviews report no gap and state that the whole manuscript was read. The review of the matrix manuscript notes that a constant in a Sobolev estimate is not sharp but is used only qualitatively, and that the manuscript cites its scalar companion only for method while reproving every step used; it adds that the result settles the one-dimensional conjecture in this range, including the scalar case, and so deserves heightened external scrutiny. The review of the equality manuscript has no minor notes.
| Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0.
|}

== Notes ==
* The earlier results are due to the authors named in the Background section, as recounted by the manuscripts; Read and Schulz's preprint precedes the manuscripts.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

The one-dimensional Lieb–Thirring conjecture - Revision history

Aftermath bot: New page: The one-dimensional Lieb–Thirring conjecture, family 262, with public follow-ups