Week of Mar 19, 2026 · Lean Weekly

Math, Inc.'s Gauss autoformalizes Viazovska's 24-dimensional sphere-packing proof in Lean

Gauss, a Math, Inc. reasoning agent built to formalize proofs automatically, produced over 200,000 lines of Lean code for Maryna Viazovska's 24-dimensional proof in two weeks, without a preexisting blueprint. The work follows the 8-dimensional formalization announced on February 23, which built on the Formalising Sphere Packing in Lean project.

Checked against: spectrum.ieee.org

Papers and events Mar 12

Axiom raises $200 million to verify AI-generated code with Lean

Axiom Quant's Series A round, led by Menlo Ventures, values the startup at $1.6 billion. Axiom trains AI systems to generate formally verified outputs in Lean and plans to scale its training infrastructure and expand its team of math experts.

Checked against: siliconangle.com

AI and formalization Mar 16

Mistral AI releases Leanstral, an open-source code agent for Lean 4

Mistral AI released Leanstral, with 6B active parameters and weights under an Apache 2.0 license. On FLTEval, a new suite built from pull requests to the FLT project, Leanstral pass@2 scores 26.3, beating Sonnet by 2.6 points while costing $36 to run versus Sonnet's $549.

Checked against: mistral.ai

Papers and events Mar 4

Renaissance Philanthropy and XTX Markets add $13.5 million to AI for Math Fund

The new commitment brings the AI for Math Fund total to $31.5 million, with grants ranging between $100,000 and $1 million to support 12-24 months of work. Applications close on March 30, 2026 at 11:59 pm PT.

Checked against: renaissancephilanthropy.org