Post #3564630
2026-03-07 15:05 UTC
🥇 @EPFL@social.epfl.ch Prof Maryna Viazovska received the 2022 Fields Medal for her work on sphere packing.
Maryna met Sidharth Hariharan in 2024 and started a Lean proof for the Sphere Packing theorems.
Now, without any additional input outside the paper and work-in-progress repo, the AI agent Gauss completed the proof for dimension 8 in 5 days, expanding the codebase from 20,000 to 60,000 lines. Dimension 24 optimality and periodic uniqueness were completed in about 2 weeks.
https://github.com/math-inc/Sphere-Packing-Lean
Replies (1)
-
@fj@mastodon.social 2026-03-17 10:29
Really nice vibe-proving model open-sourced by Mistral! Leanstral is a code agent designed for Lean 4. Leanstral is designed to be highly efficient (with 6B active parameters) and trained for operating in realistic formal repositories. Mistral also published a new evaluation suite, FLTEval, to move evaluations beyond their focus on competition math. Evaluation shows that Leanstral can translate between Rocq and Lean successfully! https://mistral.ai/news/leanstral