Our goal is to tackle pivotal and long-standing open problems in harmonic analysis, and formalize their proofs in real-time at the University of Bonn.
This shows that it is feasible for mathematicians to verify the correctness of their own proofs.
Challenges in harmonic analysis:
- Find estimates for multilinear singular integrals;
- Find new estimates and convergence results for Ergodic averages;
- Develop nonlinear analogue of Carleson’s theorem.
Our formalization will use Lean and Mathlib.
News
- This project will start April 2026.
Team
Principal Investigators
Postdocs
- Tainara Borges (starting Summer 2026)
- Stefanos Lappas (starting Spring 2026)
- Leopold Mayer (starting Summer 2026)
- Michael Rothgang
PhD Students
- Lua Viana Reis (starting Spring 2026)
Jobs
- We are looking for PhD candidates to join our project! You can apply via the BIGS website (in April or November)
- We are looking for student research assistants to join the Lean formalization effort. Contact Floris van Doorn if you are interested (only available for students in Bonn).