LEAN on Me: Transforming Mathematics Through Formal Verification, Improved Tactics, and Machine Learning ongoing
Formal proof verification can both ensure proof correctness and provide new tools and insights to mathematicians. The goals of this project include creating resources for students and researchers, verifying relevant results, improving proof tactics, and exploring Machine Learning approaches.
🧑‍🎓 Project Members
lidia.rossell (at) estudiantat.upc.edu
roehrig (at) zib.de
jaeckle (at) zib.de
🪙 Funding
This project is being funded by the Berlin Mathematics Research Center MATH+, itself funded by the German Research Foundation (DFG) under Germany's Excellence Strategy (EXC-2046/1, project ID 390685689), and the Mathematical Research Data Initiative from January 2024 to December 2025.
🔬 Project Description
Mathematics is undergoing a digital revolution with the advent of formal proof verification. This emerging field not only ensures the correctness of mathematical proofs but also offers new perspectives and tools for mathematical research. Our project aims to bridge traditional mathematics with cutting-edge computational techniques.
We are working to:
- Foster a vibrant community around formal verification in Berlin, connecting researchers and students through workshops, online resources, and university courses.
- Advance the formal verification of significant mathematical results, with a current focus on areas such as combinatorics and game theory.
- Develop and refine proof tactics, exploring the potential of optimization and machine learning techniques to enhance the efficiency of formal verification processes.
By integrating these efforts, we aim to make formal verification more accessible and powerful, potentially transforming how mathematics is taught, learned, and practiced. As we progress, we will continue to adapt our approach, always with the goal of pushing the boundaries of what’s possible in mathematical verification and discovery.