YauCounterexample

Definition

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

The block sets up a smooth Riemannian metric on the 5-manifold S^4 × S^1, where S^4 is the unit sphere in Euclidean R^5 and S^1 is the circle group, modelled on R^4 × R^1 with the product model-with-corners. SmoothMetric is a C^∞ Riemannian metric on the tangent bundle of this product. Using the standard basis of the model space, metricMatrix(g,c,y) is the Gram matrix of g applied to the pushforwards, under the derivative of the inverse of a chart c, of the basis vectors at the point y; volumeFactor is the square root of its determinant. chartLaplacian(g,c,u,y) is the coordinate expression of the Laplace–Beltrami operator in the chart: the inverse of the volume factor times the sum over i of the derivative in direction e_i of the function z ↦ volumeFactor(z) · Σ_j (metricMatrix(z)^{-1})_{ij} · ∂_j(u∘c^{-1})(z). nodalMeasure(g,u) is the 4-dimensional Hausdorff measure of the zero set {u=0}, taken with respect to the extended metric induced by the Riemannian metric g, valued in [0,∞]. MainTarget is a defined proposition, not an established theorem: it asserts that there exist a smooth metric g, positive reals λ_k, and nonzero C^∞ functions u_k on the manifold such that, in the extended chart at every point x, −Δ_g u_k = λ_k u_k, with λ_k tending to infinity and the ratio nodalMeasure(g,u_k)/√λ_k tending to ∞ in [0,∞].

Definition code

-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/YauCounterexample.lean; bytes 16..2634
-- Kind: block; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib

namespace OAI

namespace Yau
namespace Target
open Bundle Manifold Matrix Filter
open scoped ContDiff Topology ENNReal
noncomputable section

abbrev Base := Metric.sphere (0 : EuclideanSpace ℝ (Fin 5)) 1

abbrev Manifold5 := Base × Circle

abbrev Model := EuclideanSpace ℝ (Fin 4) × EuclideanSpace ℝ (Fin 1)

abbrev modelWithCorners := (𝓡 4).prod (𝓡 1)

abbrev SmoothMetric := ContMDiffRiemannianMetric modelWithCorners ∞ Model
  (fun x : Manifold5 ↦ TangentSpace modelWithCorners x)

abbrev Index := Fin (Module.finrank ℝ Model)

def frame : Module.Basis Index ℝ Model := Module.finBasis ℝ Model

def metricMatrix (g : SmoothMetric) (c : PartialEquiv Manifold5 Model)
    (y : Model) : Matrix Index Index ℝ := fun i j ↦
  g.inner (c.symm y)
    (mfderiv 𝓘(ℝ, Model) modelWithCorners c.symm y (frame i))
    (mfderiv 𝓘(ℝ, Model) modelWithCorners c.symm y (frame j))

def volumeFactor (g : SmoothMetric) (c : PartialEquiv Manifold5 Model)
    (y : Model) : ℝ := Real.sqrt (metricMatrix g c y).det

def chartLaplacian (g : SmoothMetric) (c : PartialEquiv Manifold5 Model)
    (u : Manifold5 → ℝ) (y : Model) : ℝ :=
  (volumeFactor g c y)⁻¹ * ∑ i, fderiv ℝ
    (fun z ↦ volumeFactor g c z * ∑ j,
      (metricMatrix g c z)⁻¹ i j * fderiv ℝ (u ∘ c.symm) z (frame j)) y (frame i)

def nodalMeasure (g : SmoothMetric) (u : Manifold5 → ℝ) : ℝ≥0∞ :=
  letI : RiemannianBundle (fun x : Manifold5 ↦ TangentSpace modelWithCorners x) :=
    ⟨g.toRiemannianMetric⟩
  letI : IsContMDiffRiemannianBundle modelWithCorners ∞ Model
      (fun x : Manifold5 ↦ TangentSpace modelWithCorners x) := inferInstance
  letI : MeasurableSpace Manifold5 := borel Manifold5
  letI : BorelSpace Manifold5 := ⟨rfl⟩
  letI : IsContinuousRiemannianBundle Model
      (fun x : Manifold5 ↦ TangentSpace modelWithCorners x) :=
    ⟨g.inner, g.toContinuousRiemannianMetric.continuous, fun _ _ _ ↦ rfl⟩
  letI : EMetricSpace Manifold5 := EMetricSpace.ofRiemannianMetric modelWithCorners Manifold5
  MeasureTheory.Measure.hausdorffMeasure (4 : ℝ) {x | u x = 0}

def MainTarget : Prop :=
  ∃ (g : SmoothMetric) (lam : ℕ → ℝ) (u : ℕ → Manifold5 → ℝ),
    (∀ k, 0 < lam k) ∧
    (∀ k, u k ≠ 0) ∧
    (∀ k, ContMDiff modelWithCorners 𝓘(ℝ, ℝ) ∞ (u k)) ∧
    (∀ k x, -chartLaplacian g (extChartAt modelWithCorners x) (u k) ((extChartAt modelWithCorners x) x) =
      lam k * u k x) ∧
    Tendsto lam atTop atTop ∧
    Tendsto (fun k ↦ nodalMeasure g (u k) / ENNReal.ofReal (Real.sqrt (lam k)))
      atTop (𝓝 ⊤)



end
end Target
end Yau
end OAI

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/YauCounterexample.lean

Human review

Endorsed by Community (Bot) · Oct 7, 2026
Confirmed by the moderator at approval.
Endorsed by marwahaha · Oct 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph