As part of its sponsorship program, the FMJH receives the support of Microsoft Research to promote progress in an emerging field: formalized mathematics. The FMJH is thus able to finance a one-year post-doc starting September 1st, 2022 (possibly negotiable) who will be assigned to the Laboratoire de Mathématiques d'Orsay with Patrick Massot as scientific contact. The annual net salary before taxes will be about 28 900 euros. The subject is described in detail below.
Translated with www.DeepL.com/Translator (free version)
Formalized mathematics aims to extend the mathematical toolbox through the use of softwares called proof assistants that can read and check definitions, statements and proofs. The software we will use for this project is Lean by Leonardo de Moura from Microsoft Research. The text Why formalize mathematics? by Massot and Buzzard’s ICM paper discuss some motivations for formalized mathematics and give general background. The Lean community website contains a lot of information that is more specific to Lean.
Although formalized mathematics has a long and rich history interleaved with the area of program verification, the last four years have seen a noticeable surge of activity specifically directed towards pure mathematics. Those activities had a lot of targets trying to check, explain, teach and create mathematics. All those targets are in scope for this post-doc project, but we have two main focuses:
Elementary mathematics and teaching. There are a couple of related goals here. The main one is of course to finish formalizing a standard undergrad curriculum in mathlib, Lean’s mathematics library (see mathlib’s undergrad to do list in particular). This part involves all the usual challenges of formalized mathematics, including finding the right level of abstraction, finding the most convenient encoding in dependent type theory, leveraging the implicit information inference mechanisms of Lean, and making sure that newly added topics interact smoothly with the existing ones. There is also interesting work to do in order to make it easier to use mathlib as a backend to build more specialized libraries using more elementary definitions (for instance basing real analysis on ε’s rather than Bourbaki’s theory of filters). More generally, we still need a lot of thinking to build more teaching material that is easy to use for students focussing on using a proof assistant to learn traditional mathematics rather than becoming expert users of a proof assistant. This aspect will probably involve talking to researchers in education science (interested researchers exist at least in Paris, London and Toronto).
Lean for communicating mathematics. The goal here is to use Lean to create interactive mathematical documents where readers choose the level of detail, all the way from an informal sketch to axioms, with smooth transitions. This part involves meta-programming in Lean 4, the new version of Lean that we are currently migrating to. It will probably build on the work of Bülow on LeanInk. A first step would be to improve the output of LeanInk to also give access to more information that is implicit on paper or in the code we type but is inferred by Lean from the context. This information is somewhat accessible in Lean 3 but the process is cumbersome and the output can be really difficult to read. A more ambitious goal would be to give access to all this information in mostly natural language, without requiring knowledge of Lean. Designing a nice user interface is part of the challenge.
The balance between those two main focusses will of course depend on the interest and skills of the post-doc. Formalization experience, either with Lean or with another proof assistant, is of course very welcome. But applications by highly motivated mathematicians having shown clear computer skills will also be considered.
The mathematics department in Orsay is a great place to work at, and is also surrounded with lots of other great places that are easily accessible, including the computer science department and its Formal methods lab, the IHES and the whole Paris area.