Dans le cadre de son programme de mécénat, la FMJH reçoit le soutien de Microsoft Research pour favoriser les progrès sur un domaine émergent : les mathématiques formalisées. La FMJH est donc à même de financer un post-doc d’un an à compter du 1er Septembre 2022 (possiblement négociable) qui sera affecté au Laboratoire de Mathématiques d’Orsay avec pour contact scientifique Patrick Massot. Le salaire net annuel avant impôt sera d'environ 28 900 euros. Le sujet est décrit de façon précise ci-après.
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.
La Fondation Mathématique Jacques Hadamard (FMJH) et le Labex Mathématique Hadamard (LMH) offrent des financements d'un ou deux ans pour des étudiants talentueux désireux d'effectuer un séjour post-doctoral dans l’un des laboratoires de mathématique affiliés à la 
Pour faciliter vos recherches, vous pouvez consulter 
Post-Docs FMJH - LMH / Campus Paris-Saclay
Post-Docs FMJH - LMH / Campus Paris-Saclay
Post-Docs FMJH / LMH / Université Paris-Saclay