Oct 6, 2026
Lean formalization in OpenAI math repository (Result 269)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'A Fock-space inequality and the Laughlin spectral gap'. We prove the spherical fermionic Laughlin spectral-gap conjecture for the full V1 interaction. With coefficient one for each pair projector, the gap above the Laughlin state at filling 1/3 on the round sphere is at least 1/25 for all sufficiently large systems. More generally, H_Q^2\ge\gamma H_Q for some fixed \gamma\gt 1/25 on the entire lowest-Landau-level Fock space for all sufficiently large flux Q, independently of particle number.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 269). The Lean development was not rebuilt locally.