Loading...
Organizing Committee
Carnegie Mellon University
Imperial College London
University of Freiburg
University of Toronto
Fordham University
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.
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.
Loading...
Loading participant list in background...
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