Document-Level Autoformalization
The Project
The project will develop open-source tools to automate the formalization of mathematical documents, enabling algorithmic verification of research-level mathematics using the Lean proof assistant. The project's team will leverage their experience in formalizing advanced mathematics in number theory and geometric optimization, as well as the expertise in natural language processing and formal verification. By integrating large language models with automated symbolic reasoning, the project will create a modular formalization framework based on Lean blueprints, helping to democratize the formal verification of mathematical results.
The Team
Antoine Bosselut is an assistant professor in the School of Computer and Communication Sciences at EPFL, the Swiss Federal Institute of Technology in Lausanne. Previously, he was a postdoctoral fellow at Stanford University and a Young Investigator at the Allen Institute for AI (AI2). He received his PhD at the University of Washington in 2020. His research focuses on developing AI reasoning methodologies that can be effectively translated to important societal problems in health, education, and helping underserved communities. He was named as one of the Forbes 30 under 30 list for Science and Healthcare in 2021 and is on the steering committee of the Swiss AI Initiative.
Viktor Kunčak is an associate professor in the School of Computer and Communication Sciences at EPFL, which he joined in 2007 after receiving a PhD from MIT. Since then, he has been leading the EPFL Laboratory for Automated Reasoning and Analysis, supervising 16 completed PhD theses. His group developed the Stainless software verifier and the Lisa formal proof assistant. Viktor served as an initiator and one of the coordinators of a European network (COST action) in the area of automated reasoning, verification, and synthesis and received a 5-year single-investigator European Research Council (ERC) grant of 1.5M EUR on program synthesis.
Maryna Viazovska was born in Kiev, Ukraine in 1984. She obtained her bachelor's degree in mathematics in 2005 from Kiev National University and a master's degree in 2007 from the University of Kaiserslautern. She was a doctoral student of Don Zagier in the Max Planck Institute for Mathematics and received doctoral degree from the University of Bonn. After a postdoctoral position at the Humboldt University in Berlin she joined the faculty of EPFL in 2017, where she became full professor in 2018. In 2022 she was awarded the Fields Medal for her solution of the sphere packing problem in dimension 8.