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.
Team
Principal Investigators
Postdocs
- Tainara Gobetti Borges
- Pavel Gubkin (starting Fall 2026)
- Stefanos Lappas
- Leopold Mayer (starting Fall 2026)
- Michael Rothgang
PhD Students
- Koen Bresters (starting Fall 2026)
- Pauwel Van Den Eeckhaut (starting Fall 2026)
- Lua Viana Reis
Visiting Researchers
- Polona Durcik (Summer 2026)
- Lasha Ephremidze (Summer 2026)
- Lars Niedorf (Summer 2026)
- Joris Roos (Spring/Summer 2026)
- Lenka Slavı́ková (Summer 2026)
Student Research Assistants:
- Alexander Brodbelt Lopez
- Leo Diedering
- Evgenia Karunus
- Pan Lin
- Felix Pernegger
- Mara Silge (starting Fall 2026)
Papers and Preprints
- Formalizing Carleson’s Theorem in Lean, Lars Becker, María Inés de Frutos-Fernández, Leo Diedering, Floris van Doorn, Sébastien Gouëzel, Evgenia Karunus, Edward van de Meent, Pietro Monticone, Jasper Mulder-Sohn, Jim Portegies, Joris Roos, Michael Rothgang, James Sundstrom, Jeremy Tan. arXiv preprint.
- A blueprint for the formalization of norm-variation of multiple ergodic averages for commuting transformations, Floris van Doorn, Polona Durcik, Joris Roos, Lenka Slavíková, Christoph Thiele. arXiv preprint
- Weighted Riesz–Kolmogorov criterion and multilinear extrapolation of compactness on variable Lebesgue spaces, Spyridon Kakaroumpas, Stefanos Lappas. arXiv preprint
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).