Christoph Thiele and Floris van Doorn from the University of Bonn have been awarded an ERC Synergy Grant of 6.4 million euros
Will it be possible in future to prepare proofs developed in cutting-edge mathematical research with a reasonable amount of human effort so that they can be verified by computers in real time? Prof. Dr. Christoph Thiele and Prof. Dr. Floris van Doorn from the Hausdorff Center for Mathematics (HCM), a Cluster of Excellence at the University of Bonn, want to help make this possible. The two researchers submitted a joint application for a coveted Synergy Grant from the European Research Council (ERC). Following the award of the grant, the European Union will now provide total funding of 6.4 million euros to the “Harmonic Analysis with Lean Formalization” (HALF) project over the next six years. Lean is a relatively new programming language that is increasingly establishing itself as the standard for mathematical formalization.
HALF will investigate central and long unresolved problems in harmonic analysis, whereby the main focus will be placed on multilinear and non-linear operators. These fundamental questions also have applications in other mathematical and interdisciplinary fields such as ergodic theory and quantum information processing. The new results from HALF should help mathematicians to verify proofs in the Lean language with the aid of computers.
“As the first project of its kind, HALF will mark a milestone on the path to the routine use of computer verification in mathematical research,” says Prof. Dr. Floris van Doorn from the Mathematical Institute at the University of Bonn. The researchers also aim to produce urgently needed training material for applications anticipated in the field of artificial intelligence (AI), which will support the verification process in future and provide automated tools for making rigorous discoveries in mathematics.
Formalization is important for mathematical research and AI applications
“In principle, it is possible to carefully formulate and code a mathematical proof so that a computer can certify that it is correct,” explains van Doorn’s colleague at the Mathematical Institute and Project Head Prof. Dr. Christoph Thiele. However, we are still a long way from the standard application of this formalization process. “It already works really well at the level of school mathematics,” says Thiele. “However, there is still too much effort required at a mathematical research level to prepare proofs for computer verification.”
Over the next six years Prof. Thiele will push forward with his research into harmonic analysis and formalize it in cooperation with the experts in Prof. van Doorn’s research group. The two areas of expertise of these researchers complement each other well. Both are members of the Hausdorff Center for Mathematics (HCM) Cluster of Excellence and work closely with the Transdisciplinary Research Area (TRA) “Modelling” at the University of Bonn.
“Our aim is to be able to already check that submitted research results are correct before a reviewer is asked to give their opinion on the quality of the work,” says Prof. van Doorn. It is possible that AI will yield mathematical proofs in the future. In order to be able to trust these proofs without any additional work, it is essential that the AI system can formalize them itself. Leading companies and many start-ups in the AI sector around the world are already interested in “Mathlib”, a standard library of existing fundamental mathematical knowledge at a school and university level, which is being developed by van Doorn and his colleagues and will be expanded by the contributions made by HALF in the area of harmonic analysis.
A highly regarded pilot project is leading the way
“We carried out a pilot project last year to prove that our project is feasible,” says Thiele. When his research group produced a new result in the field of harmonic analysis, van Doorn realized that it was particularly suitable for a formalization process. A famous classical result developed by L. Carleson in 1966, which had not yet been formalized, was also verified at the same time. The project required close cooperation between Thiele and van Doorn and their work was followed by many mathematicians around the world. It was also possible to complete the project much quicker than originally envisaged thanks to the assistance of a dozen volunteers from the international Lean community. The HALF project will allow this type of work to be completed within the research group itself. The researchers plan to improve and speed up the processes over time.
About the researchers:
Christoph Thiele studied mathematics at the University of Darmstadt and the University of Bielefeld, received his doctorate from Yale University and qualified for professorship at the University of Kiel. He held the position of Professor at the University of California in Los Angeles from 1998 to 2012 and since then has been Hausdorff Chair at the University of Bonn. Thiele has received numerous awards including the Salem Prize and Humbolt Research Prize and was also invited to speak at the International Congress of Mathematicians in 2002.
Floris van Doorn studied mathematics at Utrecht University and received his doctorate at Carnegie Mellon University. After carrying out research in Pittsburgh and Paris-Saclay, he took a position at the University of Bonn in 2023. He is one of the pioneers of formalization in Lean and one of the heads of the international Mathlib project. His awards include the Skolem Award, which he received this year.