Mastodawn

🥇 @EPFL 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

GitHub - math-inc/Sphere-Packing-Lean: A Lean formalisation of Maryna Viazovska's Fields Medal-winning solution to the sphere packing problem in dimension 8 and 24.

A Lean formalisation of Maryna Viazovska's Fields Medal-winning solution to the sphere packing problem in dimension 8 and 24. - math-inc/Sphere-Packing-Lean

GitHub

Kensan 9h ago

Show thread

Frédéric Jacobs

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

Leanstral: Open-Source foundation for trustworthy vibe-coding | Mistral AI

First open-source code agent for Lean 4.

Show thread

Jan Lehnardt

8h ago

@fj do they publish what went into the model?

Show thread

sam 5h ago

@fj Formal verification for AI-generated code is the right direction. Proving correctness at the function level is powerful.

The layer we focus on is different but complementary — production readiness signals: does CI exist, are there tests, is config externalized. The structural stuff that formal methods don't typically cover but that still breaks deploys.