Geometry

Green42.green_42

Can the Cohn-Elkies scheme be used to prove the optimal bound for circle-packings in 2 dimensions?

References

Gr24] [Green, Ben. "100 open problems." (2024).

[CoEl03] Cohn, Henry, and Noam Elkies. "New upper bounds on sphere packings I." Annals of Mathematics (2003): 689-714.
[Vi17] Viazovska, Maryna S. "The sphere packing problem in dimension 8." Annals of mathematics (2017): 991-1015.
[CKM17] Cohn, H., Kumar, A., Miller, S., Radchenko, D., & Viazovska, M. (2017). The sphere packing problem in dimension 24. Annals of mathematics, 185(3), 1017-1033.
[Sa21] Sardari, Naser Talebizadeh. "Higher Fourier interpolation on the plane." arXiv preprint arXiv:2102.08753 (2021).

No one has attempted this yet.

Formal statement

Lean type

True ↔ Green42.CohnElkiesOptimal 2 (√3 / 6)

What you must prove

import FormalConjectures.GreensOpenProblems.«42»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green42.green_42" := by
  sorry

end Bounty

Pinned source: FormalConjectures/GreensOpenProblems/42.lean

Source type SHA-256: sha256:90586c657f6905c747525367ba3f1e3b1edaf30fa8995276b0af724a40e43cc0
Task id: fc-379fc029-green42-green-42-8b8338f242-formalized-v1
Task commitment: sha256:9789ded62b701c8f77a0d2bd9790f57542694a2b4b59ed718613764fe148dff5

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.