Lean job in Orsay

Stream: job postings

[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.

[Patrick Massot]

I now have an official announcement at https://www.fondation-hadamard.fr/en/funding/accueil-294-postdoctoral-fellowships together with an application form at https://www.fondation-hadamard.fr/fr/content/exceptional-call-post-doc-applications

[Patrick Massot]

Don't hesitate to share those links as widely as possible.

[Eric Wieser]

Is "The annual net salary before tax will be approximately EUR 28 900" a typo / translation error? I'm used to "net" referring to the result after tax is deducted, and "gross" referring to the salary before tax.

[Riccardo Brasca]

In France people usually say "net" to mean after deduction of pension related taxes, but this is not what in practice you get in your bank account

[Riccardo Brasca]

This depends on your personal situation, like children and so on, this is why it's rarely specified

[Eric Wieser]

Are the pension related taxes the same for everyone then, and therefore not usually given in salary quotes in France? I'd be surprised to see anything but the gross rate in the US / UK.

[Patrick Massot]

I have no idea what it actually mean. A good approximation would probably to ask Floris how much he actually gets. I think this post doc is meant to be paid a bit better than Floris's.