The Coq mailing list

[Jasmin Blanchette <jasmin.blanchette AT inria.fr>]

Dear Coq users,

Lean Forward [1] 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.

As part of this project, we will develop formal libraries of fundamental 
number theory in Lean 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 contribute to the development of 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 
me for more information.

Regards,

Jasmin

[1] https://lean-forward.github.io