Sharp one-dimensional Lieb–Thirring constants

Lean formalization in OpenAI math repository (Result 262)

Model / AI: OpenAI (unreleased)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'Sharp one-dimensional Lieb–Thirring constants'. We resolve affirmatively the remaining cases of the scalar one-dimensional Lieb–Thirring conjecture: for every \frac12\lt \gamma\lt \frac32, the optimal constant is the one-bound-state constant. The estimate holds for every nonnegative potential in L^{\gamma+1/2}(\mathbb R), with all negative eigenvalues included.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 262). The Lean development was not rebuilt locally.

• Paper — Paper
• Lean — Lean formalization note
• Code — OpenAI math repository