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

January 2026

Lazar Milikic joins the project.

November 2025

Release of the version 0.10.0 of Lean Interact by Auguste Poiroux
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