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?