Future-proofing formal mathematics
Formal methods have the potential to fundamentally transform mathematical research. They already play an increasingly important role in ensuring the correctness of software and mathematics, and in the training of AI systems by verifying their output.
This research semester aims to prepare the ground for widespread adoption of formal methods in mathematics. In particular, we will focus on:
- the scalability of large libraries of formalised mathematics,
- proof automation through neural and symbolic methods,
- usability improvements to lower the entry barrier.
Supporting outcomes:
- a whitepaper with a roadmap on the future of formalised mathematics,
- an open-source textbook project on the formalisation of contemporary mathematics,
- contributions to proofs and automation to libraries of formal mathematics (such as the Mathlib library of Lean), and
- building of community and expertise both nationally and internationally.
The program will consist of:
- a four-day tutorial, Lean for the Curious Mathematician (LFTCM), for absolute beginners who are interested in Lean;
- a four-day workshop for practitioners of formalisation (including a tactic-programming tutorial and hackathon);
- a five-day conference on long-term challenges of formal methods in mathematics (scaling of the codebase, automation, usability by a broader group of mathematicians, etc.).
More information will follow.
