What was already known
Thue’s theorem already established the optimal planar packing density. Cohn and Elkies conjectured that their Fourier bound attains it exactly; numerical approximations had not proved sharpness.
AI involvement
OpenAI is credited as author of the internally produced mathematical manuscript; individual-session autonomy is undocumented.
Institutional AI authorship and collection provenance support AI-led production.
Importance
Claims an exact sharp certificate for the planar Fourier packing bound.
Limitations
This certificate does not prove uniqueness of periodic equality cases or the stronger prescribed-zero condition. A possibly related 2026 thesis claim has not been fully compared.
Technical verification
The repository reports a Lean proof of the exact normalized Fourier-certificate existence theorem. Its separate finite interval verifier checks only matrix, residual, Bernstein, and scalar comparisons; analytic parts are covered by the Lean theorem rather than that script alone.
Formal checking
Existence of a radial Schwartz function meeting the sharp planar Fourier certificate conditions. formal proof
- Checker
- Lean kernel via OAI.sharp_fourier_certificate
- Scope
- Existence of a radial Schwartz function meeting the sharp planar Fourier certificate conditions
- Basis
- Reported by the linked checker
Formal checking
Finite matrix, residual, Bernstein, and scalar comparisons used in the certificate. exact interval arithmetic
- Checker
- Project verify_all.py using python-flint
- Scope
- Finite matrix, residual, Bernstein, and scalar comparisons used in the certificate
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Default: the model-authored exposition does not establish a named human understanding of the certificate's construction.
Correction and publication history
Claims exact attainment of the Cohn–Elkies planar packing bound.
Read this published revision