Leaning and Rocq'ing
The Project
This project harnesses the power of large language models (LLMs) to facilitate translation of statements and proofs between different interactive theorem provers (ITPs), such as Lean and the Rocq Prover, as well as between different versions of the same prover, e.g., Lean 3 vs Lean 4. By enabling the conversion of proofs and libraries across these platforms, the initiative aims to create a unified library of formalized knowledge, enhancing collaboration and resource sharing within the formal methods community. This effort would not only bridge significant resources like MathLib and Mathematical Components but would also support smoother transitions during future major updates ,e.g., Lean 5.
The Team
Guillaume Baudart is a researcher at Inria in the PICUBE team at the IRIF laboratory. From 2017 to 2020 he was a research staff member at the IBM T.J. Watson Research Center in the AI Programming Models team. His research focuses on probabilistic programming, and more recently on generative AI for interactive theorem proving
Cyril Cohen is a researcher at Inria in the CASH team at LIP, ENS de Lyon. His primary research focus is on enriching the Rocq prover with mathematical knowledge. He is also one of the principal architects of the Mathematical Components library.
Nicolas Tabareau is a senior researcher at Inria, where he leads the Gallinette team in Nantes. He specializes in the development and implementation of interactive theorem provers (ITPs) and plays an active role in the ongoing development of the Rocq Prover.
Marc Lelarge is a senior researcher at Inria and a lecturer in the Computer Science Department at École Normale Supérieure. His research spans machine learning, deep learning, and graph theory, with a recent focus on generative AI for interactive theorem proving.