A research team from EPFL has been awarded funding through the AI for Math Fund, an $18 million program jointly developed to accelerate mathematical discovery through artificial intelligence.
Titled Document-Level Autoformalization, the project aims to bridge the gap between human and machine understanding of mathematics. The team will develop open-source tools that can automatically translate mathematical research papers into a precise, computer-readable format. This will enable algorithms to verify complex mathematical proofs using the Lean proof assistant, a system that checks the logical validity of mathematical arguments with complete rigor.
“By combining AI language models with symbolic reasoning, we are planning to build a flexible framework that helps both researchers and AI systems collaborate in verifying, and eventually discovering, new mathematical results.” says Viktor Kunčak, Professor and director of the Laboratory for Automated Reasoning and Analysis “This work could make high-level mathematics more transparent, accessible, and reliable across the global research community.”
The researchers bring together expertise in formal verification, natural language processing, and the formalization of advanced mathematics in areas such as number theory and geometric optimization. Their modular framework, based on Lean blueprints, will be shared openly to help democratize access to formal verification tools.
“Mathematics has long been a language of precision,” says Maryna Viazovska, Professor and director of the Chair of Number Theory. “Our goal is to teach machines to understand and communicate in that language fluently — helping uncover new insights that might otherwise remain hidden.”
The Renaissance AI for Math Fund is a joint initiative developed in partnership between Renaissance Philanthropy and founding donor XTX Markets . It supports researchers around the world who are integrating AI with mathematical reasoning, aiming to catalyze a new era of discovery. EPFL’s inclusion among the grantees underscores the institution’s leadership in both AI research and foundational science.
About the AI for Math Fund
The AI for Math Fund seeks to advance the pace and impact of math discovery by supporting projects that are important for the field, but no one academic or industry lab has the incentive to do them. The fund will support projects that (1) are less likely to happen in a business-as-usual scenario; and (2) have the potential to advance the field as a whole. These include: developing open-source, production-quality tools; increasing the size, diversity, and quality of datasets required for training AI models; and increasing the ease-of-use of tools so that they are adopted by mathematicians.