AA5 – Variational Problems in Data-Driven Applications



LEAN on Me: Transforming Mathematics through Formal Verification, Improved Tactics, and Machine Learning

Project Heads

Sebastian Pokutta, Christoph Spiegel

Project Members


Project Duration

01.01.2024 − 31.12.2025

Located at

TU Berlin


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.

External Website

Selected Publications