PhD position in Formalization of Mathematics

To apply to the position, mail freek@cs.ru.nl.

The FPS of FLT project

One of the Grand Challenges in Formalization of Mathematics is to fully formalize a proof of Fermat's Last Theorem. Formalization is the encoding of proofs in full detail in the language of a proof assistant like Coq, Isabelle and Lean. When formalizing, all details are encoded in full detail all the way from the axioms of the system, and therefore everything is guaranteed to be 100% flawless.

Formalization of a proof of Fermat's Last Theorem obviously will be a very large effort, but we are planning to make a start on this.

The PhD position

For this we are now looking for a PhD student. As is common in the Netherlands, there will be a four year full time paid position, click this link for information on doing a PhD at the Radboud University. At the end of the four years a PhD thesis will have been written. Part of the work will be to assist with teaching in our institute, but most of the time will be for doing research, visiting summer schools, workshops and conferences (to grow and to present papers), and writing the thesis.

We would like to have the PhD student start as soon as possible, but the start date of the position is negotiable.

In our own department several PhD students and staff members use the proof assistant Coq, but for computer science applications. The PhD student will actively participate in the user community of the proof assistant used for the project. The student will also collaborate with some mathematicians that are interested in this project outside Nijmegen.

• has a master in mathematics, and
• has an interest in formalization of mathematics.

Experience with algebraic number theory and/or proof assistants is a plus.

If you have any questions about this, then send mail to freek@cs.ru.nl.

The project

At first, no proofs will be formalized. The goal is to make a Formal Proof Sketch of an existing overview of a proof of Fermat's Last Theorem. A Formal Proof Sketch is a formalization in which details of proofs have been omitted (in many systems this means that subproofs have been replaced by "sorry" or "admit"; but Formal Proof Sketches still have a notion of correctness, in the sense that it should be possible to complete it into a formalization by supplying those details). The goal of a Formal Proof Sketch is to match an existing (non-formal, English) mathematical text as closely as possible.

In this case the game will be to

• take an existing outline of a proof of Fermat's Last Theorem (of the order of ten to twenty pages), and
• make a list of all statements in that text. Then,
• formally define all notions occuring in those statements in the language of a proof assistant (at first omitting all proofs, including those that are part of those definitions). Then,
• using these definitions, for each statement in the list write down a formal counterpart in the language of the proof assistant.

As a second step in the project, using these defintions, the top level structure of the proof will be properly formalized, taking the theorems that this is based on as axioms.

This project will be useful for two reasons:

• It will reduce formalization of a proof of Fermat's Last Theorem to "filling in the gaps". In other words, it will make it possible to divide the work and hand out pieces of it.
• It will demonstrate to mathematicians who are not familiar with formalization, what kind of mathematics is formalizable (all of it), and what the rendering of mathematics in the language of a proof assistant looks like.

The proof assistant to be used for this project probably will be Lean, as Kevin Buzzard will be working on formalization of Fermat's Last Theorem in Lean, and we will try to fit in with his project. However, if the candidate for the PhD position insists on using a different system, this is negotiable.