AI for Math @ EPFL

Document-Level Autoformalization

This project creates 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. See also the announcement of our project by the EPFL AI center.

Released software

LeanFlow document-level autoformalization agent
LeanProbe MCP server, CLI and API
Lean Interact with User Guide

Selected Publications

LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization, AI for Math @ ICML 2026 (poster)
Progress in Formalizing Sphere Packing in Dimension 8
Reliable Evaluation and Benchmarks for Statement Autoformalization, EMNLP 2025
RLMEval: Evaluating Research-Level Neural Theorem Proving, Findings of EMNLP 2025

Research Staff

Auguste Poiroux

Lazar Milikic

Principal Investigators

Antoine Bosselut

Viktor Kunčak

(contact PI)

Maryna Viazovska

News about Project and Project Members

June 2026

The paper LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization co-authored by Lazar Milikic, Simon Guilloud, Khanh Nguyen, and Viktor Kunčak was accepted at the AI for Math ICML 2026 workshop. Lazar Milikic will attend the workshop in Seoul to present the paper. It documents LeanFlow agent, and its use in several autoformalization tasks, including autoformalization of two previously not formalized results:
- Parametrization of Pythagorean Triples by a Single Triple of Polynomials (Frisch & Vaserstein, 2007)
- A Calculus Proof of the Cramer-Wold Theorem (Lyons & Zumbrun, 2017), which also produced reusable PhysLib infrastructure for distributional Laplacians of norm-kernel fundamental solutions, merged into Physlib
Lazar Milikic releases LeanProbe MCP server, CLI and API. LeanProbe enables AI agents to receive verifiable feedback about Lean proof outcomes
Lazar Milikic uses LeanFlow as well as locally deployed and frontier models to tackle benchmarks in AI for Math ICML 2026 workshop, finishing second in the leaderboard track for Theoretical Computer Science Proving in Lean.
A popular angle on aspects of sphere packing formalization and Gauss autoformalization was presented in a New York Times article from 8 June.

April 2026

A report on combining human effort and autoformalization (using Gauss) for sphere packing proof in 8 dimensions is documented in the the arxiv report Progress in Formalizing Sphere Packing in Dimension 8 with authors from the present project including Auguste Poiroux and Maryna Viazovska.

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

September 2025

Auguste Poiroux presented the work on Evaluating Research-Level Neural Theorem Proving at AITP 2025 in Aussois, France

Further Links

Selected EPFL Faculty Collaborators

Ola Svensson

Emmanuel Abbe

This project is supported by the AI For Math Fund, which is run by Renaissance Philanthropy and funded by XTX Markets.

Historical note: this project was conceived in early 2025 and approved in summer 2025.