Fwd: Lean Job in Orsay

[Siddhartha Gadgil]

---------- Forwarded message ---------
From: Siddhartha Gadgil <gad...@iisc.ac.in>
Date: Mon, 2 May 2022 at 09:55
Subject: Lean Job in Orsay
To: ALL @ MATH <all....@iisc.ac.in>

In case anyone is interested. This was posted on the Lean Prover chat

regards,

Siddhartha

Posted by Patrick Massot:

Microsoft research is funding a one year post-doc position to work with me in Orsay, France. The general area is of course formalization of mathematics. More specifically, there are 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 (see the undergrad todo list in particular). But 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 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 Lean.

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 proof terms, with smooth transitions. This part involves meta-programming in Lean 4. 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 the extra information that we can get from widgets in Lean 3 and also more information about what the elaborator is doing. This information is somewhat accessible in Lean 3 mathlib using the show_term tactic but 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.

I know the timing isn't great, administrative things went slowly. There could be some flexibility in the dates, but the idea is to work during the 2022-2023 academic year.

The mathematics department in Orsay is a great place to work at, and we are also surrounded with lots of other great places that are easily accessible. Don't hesitate to ask me questions about this offer. I hope an official advertisement will appear really soon, all administrative hurdles seem cleared now.