PhD position in Formalization of Mathematics

To apply to the position, click the red "apply" button at the top and bottom of:

The PhD position

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.

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.

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 FPS of FLT 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

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:

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 might be negotiable.