With this project, Dahmen aims to take an important step toward making complex mathematics more reliable. Together with his colleagues, he will work on a way to digitally verify complicated mathematical proofs. Ultimately, this could contribute to safer software, better cryptography, and more reliable AI systems.
Proof assistants
At the center of the project are so-called proof assistants: software programs that check mathematical theorems and their proofs in a strictly formal language. Whereas mathematicians traditionally rely on human verification, such a system can examine step by step whether a proof is correct. This makes it possible to almost completely eliminate errors.
The technology already has practical applications. Proof assistants are used, for example, to verify whether crucial software - such as compilers, aircraft control systems, or cryptographic protocols - really works without errors. They can also help assess mathematical results generated by artificial intelligence.
Dahmen focuses on a particularly difficult type of mathematical problem: Diophantine equations. These are polynomial equations in integers, a field of study that is centuries old but still plays a central role in modern number theory. Methods for solving them are often important for other disciplines as well, such as geometry and cryptography.
“The problem is that modern research on these equations combines abstract theory with advanced computer calculations. Those calculations are hardly integrated into current proof assistants. As a result, it is difficult to fully verify recent mathematical results in this area digitally,” Dahmen explains.
Certificate approach
Dahmen’s team aims to bridge this gap. The researchers will develop new methods to incorporate both the theory and the necessary computations into proof assistants. They will use a so-called certificate approach: external computing programs perform the calculations, after which proof assistants automatically verify whether the results are correct. If successful, this will create a digital library in which important parts of modern number theory are formally recorded. Such libraries could be used and expanded by researchers worldwide.
According to Dahmen, this could increase the reliability of mathematical knowledge and make it more accessible. The impact may extend beyond academia: the same techniques could contribute to stronger cryptography and more reliable digital systems - technologies that play an increasingly important role in society.
About Sander Dahmen
Sander Dahmen is associate professor in the Department of Mathematics. Before receiving this Vici grant, he had already been awarded both a Veni and a Vidi grant, in addition to other national and EU grants. Some of those projects are still ongoing, such as the Horizon Europe Marie Skłodowska-Curie Doctoral Network COGENT, which aims to train 13 PhD candidates and in which Dahmen is involved as a work-package leader. He also enjoys connecting research and teaching, and recently completed an SKO project focused on community building within the bachelor’s program in Mathematics.