Organizing Committee
Abstract

Interactive theorem proving software can check, manipulate, and generate proofs of mathematical statements, just as computer algebra software can manipulate numbers, polynomials, and matrices. Over the last few years, these systems have become highly sophisticated and have learnt a large amount of mathematics. One has to be open to the idea these systems will change the way mathematics is done, and how it is taught in universities.

At the ICERM workshop "Lean for the Curious Mathematician 2022", experts in the Lean theorem prover will explain how to do number theory, topology, geometry, analysis, and algebra in the Lean theorem prover. This will be accessible to mathematicians without a specific background in computer-proof systems. The material covered will range from undergraduate mathematics to modern research. Participants will be invited to begin formalizing mathematical objects from their own research.

Application Deadline: March 7, 2022.

Image for "Lean for the Curious Mathematician 2022"

Confirmed Speakers & Participants

Talks will be presented virtually or in-person as indicated in the schedule below.

  • Speaker
  • Poster Presenter
  • Attendee
  • Virtual Attendee

Workshop Schedule

Subscribe (iCal) Print View
Customize
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 (Immediately After Talk)
    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 .

ICERM local time in Providence, RI is Eastern Daylight Time (UTC-4). Would you like to switch back to ICERM time or choose a different custom timezone?

Customize