#spherepacking — Public Fediverse posts

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

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

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

Join us now in #L1 in the #oxford #maths #institute for a wonderful talk by Matthew Jenssen on #spherePacking from his new paper!! https://invariants.org.uk