Lean formalization in OpenAI math repository (Result 350)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Smooth counterexamples to Yau's nodal upper bound in dimensions three and four'. We construct a smooth metric on the three-sphere, arbitrarily close to the round metric in the smooth topology, and a smooth metric on S^2\times\mathbb T^2 for which sequences of exact real Laplace eigenfunctions have unbounded nodal measure divided by the square root of the eigenvalue. Each sequence belongs to one fixed metric. Thus the upper-bound part of Yau's nodal conjecture fails for smooth metrics in dimensions three and four.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 350). The Lean development was not rebuilt locally.