The Department of Mathematics of Vrije Universiteit Amsterdam welcomes applications for a fully-funded, 4-year PhD position in Number Theory and Formalization. The preferred starting date is in the period 1 May - 1 September 2022. The candidate will conduct research on Sander Dahmen's NWO-funded project "Formalizing Diophantine algorithms". This amounts to both developing and formalizing (with a proof assistant such as Lean or Coq) number theory necessary for solving Diophantine problems. The focus will be on effective/algorithmic number theory, but more "pure" results will (necessarily) also play an important role. We note that in this project most of the time will likely be spent on actual formalization work and that the proof assistant to be used will probably be Lean (but that is open for discussion). The position also contains a small teaching component. The research will be embedded in the Algebra and Number Theory group of the Mathematics Department and in particular connects to the CAN-endowed chair "Automated verification of mathematical proof" held by Assia Mahboubi. Within the Faculty of Science there will also be close collaboration with (Theoretical) Computer Science, especially the group of Jasmin Blanchette. Applications from all groups currently under-represented in academic posts are particularly encouraged. We are working to improve the present gender balance within the department, and particularly welcome applications from women. More details at https://workingat.vu.nl/ad/phd-position-number-theory-and-formalization/70lg... [For admin and other information see: http://www.mta.ca/~cat-dist/ ]