Organizing Committee
- Jeremy Avigad
Carnegie Mellon University - Kevin Buzzard
Imperial College London - Johan Commelin
University of Freiburg - Yury Kudryashov
University of Toronto - Heather Macbeth
Fordham University - Scott Morrison
Sydney University
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.

Confirmed Speakers & Participants
Talks will be presented virtually or in-person as indicated in the schedule below.
- Speaker
- Poster Presenter
- Attendee
- Virtual Attendee
-
Roza Aceska
Ball State University
-
Angelynn Alvarez
Embry-Riddle Aeronautical University
-
Nina Amla
National Science Foundation
-
Jeremy Avigad
Carnegie Mellon University
-
Matthew Ballard
University of South Carolina
-
Jon Bannon
Siena College
-
Katja Berčič
University of Ljubljana
-
Tyler Billingsley
St. Olaf College
-
Christopher Birkbeck
University College London
-
Riccardo Brasca
Université de Paris
-
Thomas Browning
UC Berkeley
-
Kevin Buzzard
Imperial College London
-
Mario Carneiro
Carnegie Mellon University
-
Antoine Chambert-Loir
Université de Paris
-
Busiso Chisala
Mzuzu University
-
Johan Commelin
University of Freiburg
-
María Inés de Frutos Fernández
Imperial College London
-
Leonardo de Moura
Microsoft
-
Moritz Doll
Universität Bremen
-
David Eisenbud
Mathematical Sciences Research Institute and University of California, Berkeley
-
Jim Fowler
The Ohio State University
-
Sam Freedman
Brown University
-
Ángel González-Prieto
Universidad Complutense de Madrid
-
Alena Gusakov
University of Waterloo
-
Sahana H Balasubramanya
University of Muenster
-
Daniel Hast
Boston University
-
Sina Hazratpour
Johns Hopkins University
-
Hans-Joachim Hein
WWU Münster
-
Daniel Hernández
University of Kansas
-
Assaf Kfoury
Boston University
-
Allen Knutson
Cornell University
-
Aleksandr Kolpakov
University of Neuchâtel
-
Alex Kontorovich
Rutgers University
-
Matthias Köppe
UC Davis
-
Yury Kudryashov
University of Toronto
-
Jaclyn Lang
Temple University
-
John Lesieutre
The Pennsylvania State University
-
Jake Levinson
Simon Fraser University
-
Robert Lewis
Brown University
-
Jireh Loreaux
Southern Illinois University Edwardsville
-
Judith Ludwig
University of Heidelberg
-
Heather Macbeth
Fordham University
-
Alba Málaga Sabogal
Université de Lorraine
-
Patrick Massot
Université Paris-Saclay at Orsay
-
Marcos Mazari-Armida
University of Colorado Boulder
-
Ryan McCorvie
California Department of Public Health
-
Dustin Mixon
Ohio State University
-
Antonio Montalban
University of California, Berkeley
-
Oliver Nash
Imperial College London
-
Filippo Nuccio Mortarino Majno di Capriglio
Institut Camille Jordan, Université Jean Monnet - Saint-Étienne (France)
-
Daniel Packer
The Ohio State University
-
Matej Penciak
Northeastern University
-
Andrew Pollington
NSF
-
Pavithra Prabhakar
National Science Foundation
-
Siobhan Roberts
Journalist
-
Elif Sacikara
University of Zurich
-
Bianca Santoro
University of Münster
-
Florent Schaffhauser
Universidad de los Andes
-
Emil Skoldberg
National University of Ireland, Galway
-
Haoyu Sun
University of Texas, Austin
-
Sam van Gool
Université de Paris 7
-
Bianca Viray
University of Washington
-
Michael Werman
Hebrew University
-
Tian An Wong
University of Michigan-Dearborn
-
Philip Wood
Harvard University
-
Junyan Xu
NCI
Workshop Schedule
Monday, July 11, 2022
-
8:30 - 8:50 am EDTCheck In11th Floor Collaborative Space
-
8:50 - 9:00 am EDTWelcome11th Floor Lecture Hall
- Brendan Hassett, ICERM/Brown University
-
9:00 - 10:00 am EDTOrganizer Welcome / Introduction to LeanProgram Overview - 11th Floor Lecture Hall
- Jeremy Avigad, Carnegie Mellon University
-
10:00 - 10:30 am EDTCoffee Break11th Floor Collaborative Space
-
10:30 am - 12:30 pm EDTNatural Number Game demo+exercisesTutorial - 11th Floor Lecture Hall
- Kevin Buzzard, Imperial College London
-
12:30 - 2:00 pm EDTLunch/Free Time
-
2:00 - 3:00 pm EDTWhat's been formalized?/Co-ordinate projectsGroup Presentations - 11th Floor Lecture Hall
- Heather Macbeth, Fordham University
-
3:00 - 3:30 pm EDTCoffee Break11th Floor Collaborative Space
-
3:30 - 5:00 pm EDTInstalling Lean + Natural Number Game exercisesTutorial - 11th Floor Lecture Hall
-
5:00 - 6:30 pm EDTReception11th Floor Collaborative Space
Tuesday, July 12, 2022
-
9:00 - 10:00 am EDT
-
10:00 - 10:30 am EDTCoffee Break11th Floor Collaborative Space
-
10:30 am - 12:30 pm EDT
-
12:30 - 2:00 pm EDTLunch/Free Time
-
2:00 - 3:00 pm EDTSets and FunctionsTutorial - 11th Floor Lecture Hall
- Mario Carneiro, Carnegie Mellon University
-
3:00 - 3:30 pm EDTCoffee Break11th Floor Collaborative Space
-
3:30 - 5:00 pm EDT
Wednesday, July 13, 2022
-
9:00 - 10:00 am EDT
-
10:00 - 10:30 am EDTCoffee Break11th Floor Collaborative Space
-
10:30 am - 12:25 pm EDTCode review for projectsTutorial - 11th Floor Lecture Hall
-
12:25 - 12:30 pm EDTGroup Photo (Immediately After Talk)11th Floor Lecture Hall
-
12:30 - 2:00 pm EDTLunch/Free Time
-
2:00 - 3:00 pm EDTTopological hierarchyTutorial - 11th Floor Lecture Hall
- Patrick Massot, Université Paris-Saclay at Orsay
-
3:00 - 3:30 pm EDTCoffee Break11th Floor Collaborative Space
-
3:30 - 5:00 pm EDT
Thursday, July 14, 2022
-
9:00 - 10:00 am EDTElementary number theoryTutorial - 11th Floor Lecture Hall
- María Inés de Frutos Fernández, Imperial College London
-
10:00 - 10:30 am EDTCoffee Break11th Floor Collaborative Space
-
10:30 am - 12:30 pm EDTUsing Lean for TeachingPanel 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 EDTLunch/Free Time
-
2:00 - 3:00 pm EDT
-
3:00 - 3:30 pm EDTCoffee Break11th Floor Collaborative Space
-
3:30 - 5:00 pm EDT
Friday, July 15, 2022
-
9:00 - 10:00 am EDT
-
10:00 - 10:30 am EDTCoffee Break11th Floor Collaborative Space
-
10:30 am - 12:30 pm EDT
-
12:30 - 2:00 pm EDTLunch/Free Time
-
2:00 - 3:00 pm EDTTowards algebraic geometryTutorial - 11th Floor Lecture Hall
- Kevin Buzzard, Imperial College London
-
3:00 - 3:30 pm EDTCoffee Break11th Floor Collaborative Space
-
3:30 - 5:00 pm EDTProject/ exercisesTutorial - 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?
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.