SLMath will award research memberships in the one-month AxIOM Building the Mathematical Library of the Future, which will be held March 15 - April 9, 2027. 

A challenging aspect of computer formalization is formalizing definitions that are (i) mathematically correct (something that is not automatically verifiable and must be checked by human experts), (ii) optimized for usability and (iii) at the appropriate level of generality. This AxIOM will focus on formalizing definitions in Lean across a wide range of mathematical subject areas in the hope that it will be possible to correctly formalize the statements of recent theorems from the research literature. Such work is essential for making formal verification tools more relevant to mathematics researchers.

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.  SLMath will provide local accommodation or reimburse participants for out-of-pocket lodging costs.

Deadline: Complete applications, including a letter of support, must be submitted by March 31, 2026.

Eligibility: Researchers with a PhD (or equivalent) or advanced graduate standing at the time of the AxIOM.

The Simons Laufer Mathematical Sciences Institute (SLMath), formerly MSRI, has been supported from its origins by the U.S. National Science Foundation, joined by other government agencies, over 110 Academic Sponsor departments, private foundations and corporations, and generous and farsighted individuals.