Zulip Chat Archive

Stream: job postings

Topic: Two part-time positions at University College London


John Talbot (Oct 20 2025 at 09:46):

We are pleased to advertise two part-time positions to work on our AI for Math Fund project :
https://www.renaissancephilanthropy.org/domain-specific-documentation-for-mathlib-1

The project aims to encourage mathematicians curious about formalization into the field by creating accessible, domain-specific guides to theorem proving in Lean.

The roles will involve writing Lean tutorials in specific areas of pure mathematics, with plenty of concrete examples to showcase Mathlib. The precise areas of mathematics covered will depend on the candidates.

We are looking for current PhD students or recently graduated PhDs with a passion for Lean.

The positions are each initially for 100 hours over the next 6 - 10 months (so between 2 - 4 hours per week).

The job advert with link to the application process is here

Please email us with any questions:
John Talbot
Richard Hill


Last updated: Dec 20 2025 at 21:32 UTC