AI for Math @ EPFL

Now available: LeanInteract User Guide

Document-Level Autoformalization

This project will create open-source tools to automate the formalization of mathematical documents, enabling algorithmic verification of mathematical results using the Lean proof assistant. The project's team leverages their experience in formalizing advanced mathematics in number theory and geometric optimization as well as expertise in natural language processing and formal verification. The approach integrates large language models (LLMs) and automated symbolic reasoning to develop a modular approach to formalization based on Lean blueprints, contributing to the democratization of formal verification of mathematics.

Funding: The project is funded by the AI for Math Fund from Renaissance Philanthropy, which has a dedicated project page. See also the announcement of our project by the EPFL AI center.

News about Project and Project Members

March 2026

Auguste Poiroux and Maryna Viazovska present form on mathematics formalization and autoformalization at the Swiss Mathematical Society Spring Meeting: Formalization and Proof Assistants
Tito Sacchi, working on formalization and proofs related to sphere packing visits Maryna Viazovska's group
The group hosts the visit of Sidharth Hariharan, an iniator of the effort to formalise Maryna Viazovska's solution to the Sphere Packing Problem in Dimension 8.
Lazar Milikic, in collaboration with groups at EPFL, fine-tunes the Swiss Apertus LLM, developing capabilities to generate Lean proofs which were entirely absent from the base model
Math, Inc releases OpenGauss, which builds on Hermes Agent as well as lean4-skills
Automated formalization of sphere packing in 24 dimensions using Gaus agent
Auguste Poiroux works on Math, Inc. on Gaus agent, leading to automated completion of the formalization of sphere packing in 8 dimensions

February 2026

Maryna Viazovska, Viktor Kunčak, Thomas Vidick, and Thomas Bourgeat are co-teaching a course Formal Mathematics with Lean and AI. The course includes group project autoformalizing mathematical results, background lectures on proofs and Lean, as well as guest lectures by Sidharth Hariharan and Auguste Poiroux

Lazar Milikic joins the project.

November 2025

Release of the version 0.10.0 of Lean Interact by Auguste Poiroux
Auguste Poiroux is a founding engineer of Math, Inc., developing autoformalization agents
Lazar Milikic joined the EPFL PhD program. He is expected to contribute to the project in the near future.
Seewoo Lee, who contributes to the Sphere Packing in Lean, visited Maryna Viazovska and met with project members
Auguste Poiroux did an oral presentation at EMNL 2025 in China of the paper Reliable Evaluation and Benchmarks for Statement Autoformalization as well as RLMEval: Evaluating Research-Level Neural Theorem Proving

October 2025

Auguste Poiroux takes part in the SorryDB Hackaton
Viktor Kunčak met the leaders of the Malinca project in INRIA Paris, as part of a joint INRIA-EPFL meeting
Auguste Poiroux participated in a Malinca project meeting in Paris