Power-law violations of Yau's nodal upper bound

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 'Power-law violations of Yau's nodal upper bound'. We construct a smooth Riemannian metric on S^4\times S^1 and a sequence of real Laplace eigenfunctions whose nodal four-volume grows faster than \lambda^{1/2+\epsilon_0} for one fixed \epsilon_0\gt 0. This disproves the smooth upper-bound assertion in Yau's nodal-set conjecture and the proposed bound with an arbitrarily small positive power loss.

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

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