AxIOM

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. The AxIOM "Building the mathematical library of the future" 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. How to Apply Applications are open via MathPrograms.org between February 1 through March 31, 2026 for visits of 1 week to 4 weeks during the program dates in Spring 2027. Apply via MathPrograms.org by March 31, 2026   Eligibility  Researchers with a PhD (or equivalent) or advanced graduate standing at the time of the AxIOM program. Researchers must be in residence for at least one week, and preference may be given to those who can attend for longer periods.  Participant Support SLMath will provide local accommodation or reimburse participants for out-of-pocket lodging costs. SLMath is committed to maintaining family-friendly policies and, when possible, facilitating appropriate arrangements for partners and children of program members. Learn more about Childcare Grants for members with children ages 17 and under. Application Requirements Curriculum Vitae Publication list Statement of purpose One letter of support