Building the Mathematical Library of the Future

[Emily Riehl]

Dear all,

We are excited to announce a month-long mathlib-focussed workshop "Building the Mathematical Library of the Future" at SLMath (formerly MSRI) from March 15th to April 9th, 2027. The workshop will be one of the first "AxIOM"s run by SLMath.

The workshop is a subject-agnostic mathematics hackathon. Our vision to bring together Lean experts across mathematics into one physical place, to see what happens. The goal is to develop and merge material needed to ensure that mathlib is able to meet the needs of the mathematical community. Formalization of mathematics is currently a very fast-moving and dynamic area, and the organizers are well-aware that it is actually difficult to predict what exactly the main problems will be this time next year.

Ideal participants will have prior experience with computer formalization and a particular subject area in which they would like to make contributions to Mathlib. An explicit goal of the workshop is to grow the Lean community, so if you have a genuine interest in dedicating time to this, please consider applying to participate. 

Note the following comment on the application form: "These positions are reserved for researchers who will be in residence for at least one week, and preference may be given to those who can attend for longer periods. “ We urge groups of people working in the same area to coordinate visit times to maximise the utility of this opportunity.

Applications are now open, and will close on 31st March 2026 (the SLMath website does not specify a time). For more details, including how to apply, see https://www.slmath.org/axiom/412#overview_axiom .

Note that SLMath asks for a CV, list of publications, statement of purpose, and also a letter of support from someone else; if you are a young researcher then we suggest that you ask someone who is writing reference letters for you, and if you are an established researcher then just ask someone else working in your field.

For the organizers:

Kevin Buzzard, Imperial College, London

Jireh Loreaux, Southern Illinois University Edwardsville

Emily Riehl, Johns Hopkins University

Adam Topaz, University of Alberta

--

Kelly Miller Professor of Mathematics (she/her)
Johns Hopkins University
emilyriehl.github.io