Yau’s nodal bounds: surfaces and higher dimensions

3 papersLean

Proves the sharp \(C\sqrt\lambda\) upper bound for nodal length on every fixed smooth closed surface, completing Yau's conjecture there. The upper bound fails for fixed smooth metrics in dimensions three and four, including metrics on S³ arbitrarily close to round. In dimension five, nodal measure can grow faster than \(\lambda^{1/2+\varepsilon_0}\) for some fixed \(\varepsilon_0\gt 0\), ruling out even arbitrarily small power losses.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 3

Sharp nodal length on smooth surfaces

OpenAI · September 23, 2026

We prove that a nonzero real Laplace eigenfunction with eigenvalue λ > 0 on a fixed smooth closed connected Riemannian surface has nodal length at most \(C\sqrt\lambda\). Together with the known lower bound, this proves Yau's conjecture in this setting.

Read PDF Download Source

Cite

@misc{OAI:Sharp-nodal-length-on-smooth-surfaces-September-23-2026,
  author = {{OpenAI}},
  title = {{Sharp nodal length on smooth surfaces}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Sharp-nodal-length-on-smooth-surfaces-September-23-2026/paper.pdf}{OAI:Sharp-nodal-length-on-smooth-surfaces-September-23-2026}},
  year = {2026}
}

Smooth counterexamples to Yau's nodal upper bound in dimensions three and four

OpenAI · September 23, 2026

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.

Read PDF Download Source

Cite

@misc{OAI:Smooth-counterexamples-to-Yaus-nodal-upper-bound-in-dimensions-three-and-four-September-23-2026,
  author = {{OpenAI}},
  title = {{Smooth counterexamples to Yau's nodal upper bound in dimensions three and four}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Smooth-counterexamples-to-Yaus-nodal-upper-bound-in-dimensions-three-and-four-September-23-2026/paper.pdf}{OAI:Smooth-counterexamples-to-Yaus-nodal-upper-bound-in-dimensions-three-and-four-September-23-2026}},
  year = {2026}
}

Power-law violations of Yau's nodal upper bound

OpenAI · September 23, 2026

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.

Read PDF Download Source

Cite

@misc{OAI:Power-law-violations-of-Yaus-nodal-upper-bound-September-23-2026,
  author = {{OpenAI}},
  title = {{Power-law violations of Yau's nodal upper bound}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Power-law-violations-of-Yaus-nodal-upper-bound-September-23-2026/paper.pdf}{OAI:Power-law-violations-of-Yaus-nodal-upper-bound-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

Yau's nodal-set conjecture predicts nodal size of order \(\sqrt\lambda\) for Laplace eigenfunctions of eigenvalue \(\lambda\). The formalization proves the upper bound on every fixed smooth closed connected Riemannian surface: there is a surface-dependent constant \(C\) such that the one-dimensional Hausdorff measure of the zero set of every nonzero real eigenfunction with \(\lambda>0\) is at most \(C\sqrt\lambda\). The known lower bound is not part of this selected statement.

The formalized results contradict Yau's proposed \(O(\sqrt\lambda)\) upper bound for nodal measure in dimensions three and four. On \(S^3\), every prescribed smooth neighborhood of the round metric contains one fixed smooth metric with an eigenfunction sequence of unbounded nodal-measure ratio. A second fixed metric on \(S^2\times T^2\) has the same property. In both cases the eigenvalues tend to infinity and the intrinsic nodal measures are finite.

Yau's nodal upper-bound conjecture predicts that the nodal measure of an eigenfunction is bounded by a constant times the square root of its eigenvalue. The formalized counterexample fixes one smooth metric on \(S^4\times S^1\) and a sequence of nonzero smooth eigenfunctions whose positive eigenvalues tend to infinity, while the intrinsic four-dimensional nodal measures divided by the square roots of the eigenvalues tend to infinity. The metric is fixed throughout the sequence.

Comparator links

Result	Comparator statement
Sharp upper bound for nodal length on smooth surfaces	NodalLength.lean
Nodal counterexamples in dimensions three and four	SmoothYau.lean
Unbounded nodal ratio on \(S^4\times S^1\)	YauCounterexample.lean

Scope note on GitHub →