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

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 .

Request Reimbursement

This section is for general purposes only and does not indicate that all attendees receive funding. Please refer to your personalized invitation to review your offer.

ORCID iD
As this program is funded by the National Science Foundation (NSF), ICERM is required to collect your ORCID iD if you are receiving funding to attend this program. Be sure to add your ORCID iD to your Cube profile as soon as possible to avoid delaying your reimbursement.
Acceptable Costs
  • 1 roundtrip between your home institute and ICERM
  • Flights on U.S. or E.U. airlines – economy class to either Providence airport (PVD) or Boston airport (BOS)
  • Ground Transportation to and from airports and ICERM.
Unacceptable Costs
  • Flights on non-U.S. or non-E.U. airlines
  • Flights on U.K. airlines
  • Seats in economy plus, business class, or first class
  • Change ticket fees of any kind
  • Multi-use bus passes
  • Meals or incidentals
Advance Approval Required
  • Personal car travel to ICERM from outside New England
  • Multiple-destination plane ticket; does not include layovers to reach ICERM
  • Arriving or departing from ICERM more than a day before or day after the program
  • Multiple trips to ICERM
  • Rental car to/from ICERM
  • Flights on a Swiss, Japanese, or Australian airlines
  • Arriving or departing from airport other than PVD/BOS or home institution's local airport
  • 2 one-way plane tickets to create a roundtrip (often purchased from Expedia, Orbitz, etc.)
Travel Maximum Contributions
  • New England: $250
  • Other contiguous US: $750
  • Asia & Oceania: $2,000
  • All other locations: $1,500
  • Note these rates were updated in Spring 2022 and superseded any prior invitation rates. Any invitations without travel support will still not receive travel support.
Reimbursement Requests

Request Reimbursement with Cube

Refer to the back of your ID badge for more information. Checklists are available at the front desk and in the Reimbursement section of Cube.

Reimbursement Tips
  • Scanned original receipts are required for all expenses
  • Airfare receipt must show full itinerary and payment
  • ICERM does not offer per diem or meal reimbursement
  • Allowable mileage is reimbursed at prevailing IRS Business Rate and trip documented via pdf of Google Maps result
  • Keep all documentation until you receive your reimbursement!
Reimbursement Timing

6 - 8 weeks after all documentation is sent to ICERM. All reimbursement requests are reviewed by numerous central offices at Brown who may request additional documentation.

Reimbursement Deadline

Submissions must be received within 30 days of ICERM departure to avoid applicable taxes. Submissions after thirty days will incur applicable taxes. No submissions are accepted more than six months after the program end.