Their dissertation is titled "Formalizing Fundamental Algebraic Number Theory". It is part of an interdisciplinary collaboration between Computer Science and Mathematics, and was supervised by Jasmin Blanchette (CS) and Sander Dahmen (Math).
Mathematicians often use a computer program for difficult or tedious computations, because computers can work quickly and precisely with numbers. But there are also programs that help with logical reasoning: proof assistants. Anne Baanen used their experience as programmer and mathematician to make proof assistants more understandable and useful.
Proof assistants check every step of a mathematical proof to verify it is correct, because a small mistake could ruin the whole effort. Using a proof assistant is difficult and time consuming: every detail has to be made precise, and computers do not have the common sense and intuition that a mathematician uses to understand a proof. Baanen sent the computers to 'maths class' to give them this required knowledge.
Baanen learned and designed many techniques for translating mathematics on paper to something a proof assistant understands. Just like for human language, something might both be correct and sound strange. Sometimes they could find a different phrasing that worked much better, or they could expand the computer language. For example, human mathematicians often reason as follows: the current situation looks exactly like something we saw before, so we can re-use what we did then. The proof assistant doesn't always see this connection. Every time it had to be 'explained' why earlier results still apply. Eventually, they found a new way to describe the situation, so the computer could understand.
To perform the research, Baanen contributed with a group of collaborators to Mathlib, a 'virtual library of mathematics'. They looked at algebraic number theory. For this, they converted (both pre-existing and specifically for the project designed) mathematical works into thousands of lines of code. In the translation process they investigated where the difficulties lay in teaching something to the computer, and how this could be made easier. For this, Baanen also studied the logical foundations of the Lean proof assistant.
Thanks to the research, mathematicians are able to check more and more complicated results. Courses where students learn logical reasoning for the first time, can already be taught using a proof assistant. In addition, there are applications in improving artificial intelligence, such as ChatGPT, which is not designed for performing logical reasoning.