OpenAI claim summary for Phys-66

A Laughlin gap stable under every small bounded scalar perturbation

OpenAI's claim

OpenAI presents a proof in the selected manuscript. The expanding-sphere Laughlin gap and unique ground state are claimed stable under small bounded projected scalar disorder, uniformly over profiles and particle number.

Mathematical statement of the claimed result

Result 1.

Let $q=3(N-1)$, $U_q$ be the spin-$q/2$ lowest Landau level on a sphere of area $2\pi q$, and \[ H_{N,q}=\sum_{i<j}P_{ij}^{(1)}\quad\text{on }\bigwedge^NU_q, \] where each projector selects pair total spin $q-1$. Perturb by $\lambda\sum_iT_q(\varphi)^{(i)}$, with $T_q(\varphi)=\Pi_qM_\varphi\Pi_q|_{U_q}$. The source claims constants $\lambda_*,\Delta_*>0$, $N_*<\infty$, such that \[ E_1(N,\lambda,\varphi)-E_0(N,\lambda,\varphi)\ge\Delta_* \] for every $N\ge N_*$, bounded real measurable $\varphi$ with $\|\varphi\|_\infty\le1$, and real $|\lambda|\le\lambda_*$. Eigenvalues count multiplicity, so the ground state is unique.

Outline of the argument

A local lowest-Landau-level calculus tracks pinned zeros and weighted observables. Orthogonal branch readout, charge bounds, and rotation averaging control local removal of interaction energy; the unperturbed Fock-space gap then absorbs the bounded perturbation.

Formal verification

For family 269, the documented entries give unperturbed spherical Laughlin and stronger Fock-space gap inequalities. Stability against scalar one-body disorder and uniqueness of the perturbed ground state are not included. The listed Comparator files are Laughlin.lean, LaughlinFock.lean, LaughlinGap.lean, LaughlinPlanar.lean. Named declarations include OAI.Laughlin.mainTarget_proved. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources

• OpenAI, Uniform Stability of the Spherical Laughlin Gap, 2026-10-05; citation key OAI:Uniform-Stability-of-the-Spherical-Laughlin-Gap-October-5-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• Family 269: Lean scope.
• Comparator Laughlin.json.
• Comparator Laughlin.lean.
• Comparator LaughlinFock.json.
• Comparator LaughlinFock.lean.
• Comparator LaughlinGap.json.
• Comparator LaughlinGap.lean.
• Comparator LaughlinPlanar.json.
• Comparator LaughlinPlanar.lean.
• OpenAI catalogue entry.