## Several PhD Positions on Verified Mathematics at VU Amsterdam, the Netherlands

Lean Forward is an ambitious research project that aims at formally proving theorems in research mathematics and to address the main usability issues hampering the adoption of proof assistants in mathematical circles, by collaborating with number theorists. The project is funded by an NWO Vidi grant from January 2019 to December 2023 and is hosted by the Vrije Universiteit Amsterdam.

We will use Lean, an exciting new proof assistant developed at Microsoft Research (Leonardo de Moura) and Carnegie Mellon (Jeremy Avigad). Lean draws on decades of experience in interactive and automatic theorem provers, including Coq, Isabelle, and Z3. Its logic is very expressive, and emphasis is placed on strong proof automation. The system is easy to extend via metaprograms that rely on the same logical language that is used to express specifications and proofs.

As part of this project, we will develop formal libraries of fundamental number theory and explore how to automate proof search in these. Moreover, we will develop techniques and tools that help mathematicians perform accurate computations and reasoning using proof assistants, integrating procedures from computer algebra systems in a foundational, verified fashion. The ultimate aim is to develop a proof assistant that actually helps mathematicians by making them more productive and more confident in their results.

We are looking for outstanding candidates for several fully funded, four-year PhD positions, due to start in 2019 or early 2020. Candidates should ideally have some experience with (automatic or interactive) theorem proving or mathematics and be at ease with both theory and engineering. Please contact Jasmin Blanchette for more information.