PhD Position in Number Theory and Formalization

[Andrei Popescu]

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/70lg5t