Spring 2027 AxIOM Program: Building the Mathematical Library of the Future
Four thematic programs open to visits from researchers with housing provided View this email in your browser [Simons Laufer Mathematical Sciences Institute (SLMath) logo] [https://mcusercontent.com/d58ee2e82c69809ff037f56b2/images/65b61197-ef81-f9f...] Apply for Spring 2027 AxIOM Program: Research Visits of 1 to 4 Weeks Simons Laufer Mathematical Sciences Institute (SLMath) - Berkeley, CA SLMath now invites applications to participate in a new short-term collaborative program model beginning in Spring 2027, open to visits of one to four weeks from interested researchers. AxIOM (Accelerating Innovation in Mathematics) are month-long, intensive research programs designed to accelerate innovation and introduce transformative ideas into the mathematical sciences. 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 Priority Application Deadline: March 31, 2026 Apply Now via MathPrograms Building the Mathematical Library of the Future March 15 - April 9, 2027 AxIOM Details: https://www.slmath.org/axiom/412 Apply Online: https://www.mathprograms.org/db/programs/1902 [Formalization of the definition of a fiber bundle in Lean, from the Mathlib library] AxIOM Organizers * Kevin Buzzard, Imperial College, London [Lead Organizer] * Jireh Loreaux, Southern Illinois University * Emily Riehl, Johns Hopkins University * Adam Topaz, University of Alberta Program Overview 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. Learn more about AxIOM month-long programs at SLMath, or propose a future AxIOM program. [https://mcusercontent.com/d58ee2e82c69809ff037f56b2/images/b1b0e04d-8c8d-c59...] MSRI, now the Simons Laufer Mathematical Sciences Institute (SLMath), 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. Mailing address: SLMath, 17 Gauss Way, Berkeley, CA 94720-5070 Did you receive this email from a friend? You can sign up online. You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files<https://outlook.office365.com/groups/groupsubscription?source=EscalatedMessage&action=files&smtp=categories%40mq.edu.au&bO=true&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Leave group<https://outlook.office365.com/groups/groupsubscription?source=EscalatedMessage&action=leave&smtp=categories%40mq.edu.au&bO=true&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>
participants (1)
-
Chris Marshall