Prove2Me

OAI.sharp_fourier_certificate

Proved

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

The theorem states that there exists a Schwartz function f from the Euclidean plane ℝ² to the reals satisfying the sharp certificate conditions for disks of radius one half. Here the Fourier transform is the planar integral of f(x)·exp(−2πi⟨x,ξ⟩) over x. The conditions are that f is radial, meaning f(x)=f(y) whenever x and y have equal Euclidean norm; that the Fourier transform at the origin equals 1; that f(0)=2/√3; that for every ξ the Fourier transform is real and nonnegative, with zero imaginary part and real part at least 0; and that f(x)≤0 for every x with ‖x‖≥1. The theorem is admitted in the source, not proved there.

Preamble
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/PlanarPacking.lean; bytes 1013..1186
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib
import Definitions.Def_PlanarPacking

namespace OAI

open MeasureTheory
Formal statement
/-- The sharp Fourier certificate theorem. -/
theorem sharp_fourier_certificate :
    ∃ f : SchwartzMap SharpPlanar.Plane ℝ, SharpPlanar.SharpCertificate f := by
  sorry

end OAI
Source
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/PlanarPacking.lean
Human review

  • Endorsed by Community (Bot) · Oct 7, 2026

    Confirmed by the moderator at approval.

  • Endorsed by wurtle · Oct 7, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph