Mathematical Sciences Research Institute

Home > Education > Current

Current Educational Events

  1. Summer Graduate School Formalization of Mathematics (SLMath)

    Organizers: Jeremy Avigad (Carnegie Mellon University), Heather Macbeth (Fordham University at Lincoln Center), Patrick Massot (Université Paris-Saclay)
    Some basic concepts in mathlib and the dependencies between them

    Computational proof assistants now make it possible to develop global, digital mathematical libraries with theorems that are fully checked by computer. This summer school will introduce students to the new technology and the ideas behind it, and will encourage them to think about the goals and benefits of formalized mathematics. Students will learn to use the Lean interactive proof assistant, and by the end of the session they will be in a position to formalize mathematics on their own, join the Lean community, and contribute to its mathematical library.

    Updated on May 11, 2023 02:03 PM PDT