Lean for the Curious Mathematician 2022

Institute for Computational and Experimental Research in Mathematics (ICERM)

July 11, 2022 - July 15, 2022
Monday, July 11, 2022
  • 8:30 - 8:50 am EDT
    Check In
    11th Floor Collaborative Space
  • 8:50 - 9:00 am EDT
    Welcome
    11th Floor Lecture Hall
    • Brendan Hassett, ICERM/Brown University
  • 9:00 - 10:00 am EDT
    Organizer Welcome / Introduction to Lean
    Program Overview - 11th Floor Lecture Hall
    • Jeremy Avigad, Carnegie Mellon University
  • 10:00 - 10:30 am EDT
    Coffee Break
    11th Floor Collaborative Space
  • 10:30 am - 12:30 pm EDT
    Natural Number Game demo+exercises
    Tutorial - 11th Floor Lecture Hall
    • Kevin Buzzard, Imperial College London
  • 12:30 - 2:00 pm EDT
    Lunch/Free Time
  • 2:00 - 3:00 pm EDT
    What's been formalized?/Co-ordinate projects
    Group Presentations - 11th Floor Lecture Hall
    • Heather Macbeth, Fordham University
  • 3:00 - 3:30 pm EDT
    Coffee Break
    11th Floor Collaborative Space
  • 3:30 - 5:00 pm EDT
    Installing Lean + Natural Number Game exercises
    Tutorial - 11th Floor Lecture Hall
  • 5:00 - 6:30 pm EDT
    Reception
    11th Floor Collaborative Space
Tuesday, July 12, 2022
  • 9:00 - 10:00 am EDT
    Basics
    Tutorial - 11th Floor Lecture Hall
    • Johan Commelin, University of Freiburg
  • 10:00 - 10:30 am EDT
    Coffee Break
    11th Floor Collaborative Space
  • 10:30 am - 12:30 pm EDT
    Logic
    Tutorial - 11th Floor Lecture Hall
    • Jeremy Avigad, Carnegie Mellon University
  • 12:30 - 2:00 pm EDT
    Lunch/Free Time
  • 2:00 - 3:00 pm EDT
    Sets and Functions
    Tutorial - 11th Floor Lecture Hall
    • Mario Carneiro, Carnegie Mellon University
  • 3:00 - 3:30 pm EDT
    Coffee Break
    11th Floor Collaborative Space
  • 3:30 - 5:00 pm EDT
    Algebra Tactics
    Tutorial - 11th Floor Lecture Hall
    • Heather Macbeth, Fordham University
Wednesday, July 13, 2022
  • 9:00 - 10:00 am EDT
    Structures and classes
    Tutorial - 11th Floor Lecture Hall
    • Robert Lewis, Brown University
  • 10:00 - 10:30 am EDT
    Coffee Break
    11th Floor Collaborative Space
  • 10:30 am - 12:25 pm EDT
    Code review for projects
    Tutorial - 11th Floor Lecture Hall
  • 12:25 - 12:30 pm EDT
    Group Photo
    11th Floor Lecture Hall
  • 12:30 - 2:00 pm EDT
    Lunch/Free Time
  • 2:00 - 3:00 pm EDT
    Topological hierarchy
    Tutorial - 11th Floor Lecture Hall
    • Patrick Massot, Université Paris-Saclay at Orsay
  • 3:00 - 3:30 pm EDT
    Coffee Break
    11th Floor Collaborative Space
  • 3:30 - 5:00 pm EDT
    Algebraic hierarchy
    Tutorial - 11th Floor Lecture Hall
    • Johan Commelin, University of Freiburg
Thursday, July 14, 2022
  • 9:00 - 10:00 am EDT
    Elementary number theory
    Tutorial - 11th Floor Lecture Hall
    • María Inés de Frutos Fernández, Imperial College London
  • 10:00 - 10:30 am EDT
    Coffee Break
    11th Floor Collaborative Space
  • 10:30 am - 12:30 pm EDT
    Using Lean for Teaching
    Panel Discussion - 11th Floor Lecture Hall
    • Speakers
    • Kevin Buzzard, Imperial College London
    • Robert Lewis, Brown University
    • Patrick Massot, Université Paris-Saclay at Orsay
    • Moderator
    • Oliver Nash, Imperial College London
  • 12:30 - 2:00 pm EDT
    Lunch/Free Time
  • 2:00 - 3:00 pm EDT
    Calculus
    Tutorial - 11th Floor Lecture Hall
    • Patrick Massot, Université Paris-Saclay at Orsay
  • 3:00 - 3:30 pm EDT
    Coffee Break
    11th Floor Collaborative Space
  • 3:30 - 5:00 pm EDT
    Complex analysis
    Tutorial - 11th Floor Lecture Hall
    • Yury Kudryashov, University of Toronto
Friday, July 15, 2022
  • 9:00 - 10:00 am EDT
    Manifolds
    Tutorial - 11th Floor Lecture Hall
    • Oliver Nash, Imperial College London
  • 10:00 - 10:30 am EDT
    Coffee Break
    11th Floor Collaborative Space
  • 10:30 am - 12:30 pm EDT
    Lean 4
    11th Floor Lecture Hall
    • Leonardo de Moura, Microsoft
  • 12:30 - 2:00 pm EDT
    Lunch/Free Time
  • 2:00 - 3:00 pm EDT
    Towards algebraic geometry
    Tutorial - 11th Floor Lecture Hall
    • Kevin Buzzard, Imperial College London
  • 3:00 - 3:30 pm EDT
    Coffee Break
    11th Floor Collaborative Space
  • 3:30 - 5:00 pm EDT
    Project/ exercises
    Tutorial - 11th Floor Lecture Hall

All event times are listed in ICERM local time in Providence, RI (Eastern Daylight Time / UTC-4).

All event times are listed in .