Week of Mar 5, 2026

Edition 9: 4 items published for Feb 26 to Mar 5, 2026.

Math, Inc.'s Gauss completes formal proof of sphere packing in dimensions 8 and 24

Math, Inc. used Gauss to help formally verify Maryna Viazovska's Fields Medal-winning sphere packing results, proving all remaining 8-dimensional results in 5 days and autoformalizing the 24-dimensional case in two weeks. The formalization grew from 70k to about 200k lines.

Checked against: math.inc

Lean core Mar 5

CSLib publishes contributor guide for formalizing computer science in Lean

The CSLib contributing guide covers two pillars: formalising computer science as reusable infrastructure, and code reasoning about mainstream programming languages via Boole, intermediate representations, and VC generation. Contributors who use AI must explain which tools they used in the PR description, following the Mathlib policy.

Checked against: leanprover/cslib

Lean core Mar 5

Lean publishes fifth release candidate for v4.29.0

The Lean project published v4.29.0-rc5, the fifth release candidate for the v4.29.0 release of Lean, on GitHub on March 5, 2026.

Checked against: lean4 v4.29.0-rc5

Papers and events Mar 3

Kevin Hartnett's book on Lean's history opens for pre-orders

Kevin Hartnett's forthcoming book, "The Proof in the Code," tells the story of Lean's development and rise. The book is out in June, and pre-orders are open.

Checked against: @KSHartnett on X