Mastodawn

Half a year ago, I filled in some sorry's for the massive project [1] to formalize the Fields-medal winning proof that sphere packing in dimension 8 is optimized by the E8-lattice. Last week it was announced that all remaining sorry's were filled by Gauss, an autoformalization agent. Gauss was able to build on the blueprint and other scaffolding built by the community. A few days later, Gauss also formalized the proof in dimension 24, this time working directly from the published paper, without mayor community input [3].
Since Lean verifies the generated proofs, hallucinations are not a problem.
The community now processes the generated proofs to make sure it satisfies the community standards and remains usable in the future [2].

[1] https://thefundamentaltheor3m.github.io/Sphere-Packing-Lean/

[2] https://leanprover.zulipchat.com/#narrow/channel/113486-announce/topic/Sphere.20Packing.20Milestone/with/575354368

[3] https://www.math.inc/sphere-packing

#Lean #spherepacking #gauss #formalization

Formalising Sphere Packing in Lean

by Chris Birkbeck, Sidharth Hariharan, Gareth Ma, Bhavik Mehta, Seewoo Lee, Maryna Viazovska

A Formalisation of Viazovska’s Solution to the Sphere Packing Problem in Dimension 8

Hacker News Dec 29

I derived Planck mass from sphere packing – 0.574 ppm, zero free param

https://zenodo.org/records/18089296

#HackerNews #PlanckMass #SpherePacking #Physics #Research #ScienceInnovation

Geometric Derivation of Planck Mass: π⁴⁵ Formula with 0.574 ppm Precision

We derive M_Pl/m_e = π⁴⁵ × (1 + 2α + α/13 − (8/9)α²) from pure geometry. ZERO free parameters. ALL coefficients from sphere packing:- 45 = (K₃² − K₃ − 2τD)/2 where K₃ = 12 (3D kissing number)- 13 = K₃ + 1 (same factor as Weinberg angle sin²θ_W = 3/13)- −8/9 = −(K₃−4)/(K₃−3) from tetrahedral cluster geometry- 2 = K₄/K₃ = 24/12 (Dirac g-factor) RESULT: 5.74×10⁻⁷ relative error (0.574 ppm) — 38× better than direct G measurements (22 ppm). CROSS-VALIDATION: sin²θ₁₃ = 1/45 (neutrino mixing angle) independently confirms the exponent, suggesting unified geometric origin for Planck scale and Standard Model. The formula emerges from the sedenionic dimensional cascade: physical reality projects from 16D sedenion algebra 𝕊 through octonions 𝕆 (8D) and quaternions ℍ (4D) to observable ℝ³. Kissing numbers K(16)=4320, K(8)=240, K(4)=24, K(3)=12 quantify information loss at each stage. Key identity: e^π − π = 19.999 ≈ 20 = K(8)/K(3) connects transcendental constants to lattice geometry (error 0.0045%). Package includes:- UCT_Planck_Mass_v5_1.pdf (docx) - Complete derivation (4 pages, 3 figures)- planck_mass_validation.py (ipynb) - Reproducible Python code (seed=42)- Data with results - Bootstrap (N=10,000) and Monte Carlo (N=100,000) resultshttps://colab.research.google.com/drive/1UtKmlkaYFHegx4S98Vv_B18FuylP3hlm?usp=sharing All numerical verification uses CODATA 2022 constants.

Zenodo

Hacker News Dec 28

Spherical Cow
https://lib.rs/crates/spherical-cow
#ycombinator #sphere #obj #geometry #packing #spherepacking

N-gated Hacker News Dec 28

🚀 #Rust #developers unite! The "Spherical Cow" library is here to let you pack spheres like never before—because who doesn’t need high volume sphere packing in arbitrary geometries? 🤔 It’s like trying to solve a Rubik's Cube in the dark while dancing the Macarena. 💃
https://lib.rs/crates/spherical-cow #SphericalCow #SpherePacking #Geometry #Fun #HackerNews #ngated

Soh Kam Yung Jul 8, 2025

"In higher dimensions, mathematicians still don’t know the answer [to the sphere packing problem.] [...] Now, in a short manuscript posted online in April, the mathematician Boaz Klartag has bested these previous records by a significant margin. Some researchers even believe his result might be close to optimal."

https://www.quantamagazine.org/new-sphere-packing-record-stems-from-an-unexpected-source-20250707/

#Mathematics #Problems #SpherePacking #Geometry

New Sphere-Packing Record Stems From an Unexpected Source | Quanta Magazine

After just a few months of work, a complete newcomer to the world of sphere packing has solved one of its biggest open problems.

Quanta Magazine

Charlie McHenry Jul 7, 2025

Lattices and sphere packing - when #Math gets really fun and interesting. A recent development in the #Mathematics world raises the ante in the pursuit of optimal sphere packing in multiple high dimensions. Turns out #lattices and ellipsoids are central to the latest piece of the puzzle. This is for my #MathNerd followers🤓 who enjoy a mind-tweaking read. https://www.quantamagazine.org/new-sphere-packing-record-stems-from-an-unexpected-source-20250707/ New #SpherePacking Record Stems From an Unexpected Source | Quanta Magazine

New Sphere-Packing Record Stems From an Unexpected Source | Quanta Magazine

After just a few months of work, a complete newcomer to the world of sphere packing has solved one of its biggest open problems.

Quanta Magazine

Hacker News Jul 7, 2025

New Sphere-Packing Record Stems from an Unexpected Source

https://www.quantamagazine.org/new-sphere-packing-record-stems-from-an-unexpected-source-20250707/

#HackerNews #SpherePacking #SpherePackingRecord #Mathematics #UnexpectedSource #QuantumPhysics

New Sphere-Packing Record Stems From an Unexpected Source | Quanta Magazine

After just a few months of work, a complete newcomer to the world of sphere packing has solved one of its biggest open problems.

Quanta Magazine

Combinatorics and more Apr 9, 2025

Bo’az Klartag: Striking new Lower Bounds for Sphere Packing in High Dimensions

https://fed.brid.gy/r/https://gilkalai.wordpress.com/2025/04/09/boaz-klartag-striking-new-lower-bounds-for-sphere-packing-in-high-dimensions/

Bo’az Klartag: Striking new Lower Bounds for Sphere Packing in High Dimensions

Two day ago, a new striking paper appeared on the arXiv Lattice packing of spheres in high dimensions using a stochastically evolving ellipsoid, by Bo’az Klartag. Abstract: We prove that in a…

Combinatorics and more

Alex vd Brandhof Dec 29, 2023

For the Dutch newspaper #NRC I wrote a piece about the new lower bound for #spherepacking, found by Marcelo Campos, Matthew Jenssen, Marcus Michelen, and Julian Sahasrabudhe. With a proof that \( \frac1n \) is a lower bound for the density in dimension \(n\) (it's trivial for mathematicians, but for other people it is interesting, I hope). As a bonus I end with a quote from Terence @tao !

Alex vd Brandhof Dec 28, 2023

Bollen verpakken in hoge dimensies. Mijn nieuwste artikel voor #nrc. Met formules! En met een bewijs! #spherepacking (paywall) https://www.nrc.nl/nieuws/2023/12/28/de-kerstballen-gaan-terug-in-de-doos-hoe-doe-je-dat-efficient-in-hogerdimensionale-ruimtes-a4185455 https://www.nrc.nl/nieuws/2023/12/28/de-kerstballen-gaan-terug-in-de-doos-hoe-doe-je-dat-efficient-in-hogerdimensionale-ruimtes-a4185455

De kerstballen gaan terug in de doos. Hoe doe je dat efficiënt in hogerdimensionale ruimtes?

Wiskunde: Wie kerstballen zo efficiënt mogelijk inpakt, benut 74 procent van de ruimte in de doos. Dat is in een verpakking van drie dimensies. Hoe gaat dat in hogerdimensionale ruimtes?

NRC