Oct 6, 2026
Lean formalization in OpenAI math repository (Result 347)
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 'Three fixed points on the symplectic quadric threefold'. We construct a smooth Hamiltonian diffeomorphism of the complex quadric threefold with exactly three fixed points, at least one of which is degenerate. The critical number and the unit-inclusive rational cup length of this manifold are both four. Thus the example disproves the unrestricted critical-number and rational cup-length forms of the Arnold conjecture.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 347). The Lean development was not rebuilt locally.