Home /  Summer Graduate School /  Schedule

Schedule, Notes/Handouts & Videos

Formalization of Mathematics (SLMath) June 05, 2023 - June 16, 2023

Show All Collapse
Jun 05, 2023
Monday
09:00 AM - 09:15 AM
  Introduction to SLMath
09:15 AM - 10:15 AM
  Introduction to Formalized Mathematics
Patrick Massot (Université Paris-Saclay)
10:15 AM - 11:15 AM
  Basics (Chapter 2 of MIL)
Heather Macbeth (Fordham University at Lincoln Center)
11:15 AM - 11:30 AM
  Installing Lean
Jeremy Avigad (Carnegie Mellon University)
11:30 AM - 01:30 PM
  Installing Lean on Participants' Computers and Lunch
01:30 PM - 02:15 PM
  More Basics (Chapter 2 of MIL)
Jeremy Avigad (Carnegie Mellon University)
02:15 PM - 03:30 PM
  Exercise Session
03:30 PM - 04:00 PM
  Tea
04:00 PM - 05:00 PM
  Exercise Session
Jun 06, 2023
Tuesday
09:00 AM - 10:00 AM
  Logic (Chapter 3 of MIL)
Jeremy Avigad (Carnegie Mellon University)
10:00 AM - 12:00 PM
  Exercise Session
12:00 PM - 01:30 PM
  Lunch
01:30 PM - 03:30 PM
  Sets and Functions (Chapter 4 of MIL)
Jeremy Avigad (Carnegie Mellon University), Patrick Massot (Université Paris-Saclay)
03:30 PM - 04:00 PM
  Tea
04:00 PM - 05:00 PM
  Exercise Session
Jun 07, 2023
Wednesday
09:00 AM - 10:00 AM
  Number Theory (Chapter 5 of MIL)
Heather Macbeth (Fordham University at Lincoln Center)
10:00 AM - 11:30 AM
  Exercise Session
11:30 AM - 02:00 PM
  Lunch
02:00 PM - 03:00 PM
  Lecture and Discussion
03:00 PM - 03:30 PM
  Exercise Session
03:30 PM - 04:00 PM
  Tea
04:00 PM - 05:00 PM
  Logical Foundations
Jeremy Avigad (Carnegie Mellon University)
Jun 08, 2023
Thursday
09:00 AM - 10:00 AM
  Algebraic Structures (Chapter 6 of MIL)
Thomas Browning (University of California, Berkeley)
10:00 AM - 12:00 PM
  Exercise Session
12:00 PM - 01:30 PM
  Lunch
01:30 PM - 03:30 PM
  Exercise Session
03:30 PM - 04:00 PM
  Tea
04:00 PM - 05:00 PM
  Forgetful Inheritance, Hom-Like and Set-Like
Kyle Miller (Université Paris-Saclay)
Jun 09, 2023
Friday
09:00 AM - 10:00 AM
  Topology (Chapter 8 of MIL)
Patrick Massot (Université Paris-Saclay)
10:00 AM - 12:00 PM
  Exercise Session
12:00 PM - 01:30 PM
  Lunch
01:30 PM - 02:30 PM
  Discussion of Possible Projects for Week 2
02:30 PM - 03:30 PM
  Exercise Session
03:30 PM - 04:00 PM
  Tea
04:00 PM - 05:00 PM
  Exercise Session
Jun 12, 2023
Monday
09:00 AM - 10:00 AM
  Hierarchies (Chapter 7 of MIL)
Patrick Massot (Université Paris-Saclay)
10:00 AM - 12:00 PM
  Work on Projects
12:00 PM - 01:30 PM
  Lunch
01:30 PM - 03:30 PM
  Work on Projects
03:30 PM - 04:00 PM
  Tea
04:00 PM - 05:00 PM
  Formalizing Fourier Analysis
Heather Macbeth (Fordham University at Lincoln Center)
Jun 13, 2023
Tuesday
09:00 AM - 10:00 AM
  Hierarchies (Chapter 7 of MIL) Continued, and Differential Calculus (Chapter 9 of MIL)
Patrick Massot (Université Paris-Saclay)
10:00 AM - 12:00 PM
  Work on Projects
12:00 PM - 01:30 PM
  Lunch
01:30 PM - 03:30 PM
  Work on Projects
03:30 PM - 04:00 PM
  Tea
04:00 PM - 05:00 PM
  From Lean to Informal Mathematics
Kyle Miller (Université Paris-Saclay)
Jun 14, 2023
Wednesday
09:00 AM - 11:00 AM
  Finiteness and Graph Theory
Kyle Miller (Université Paris-Saclay)
11:00 AM - 12:00 PM
  First Progress Report on Projects, Discussion
12:00 PM - 01:30 PM
  Lunch
01:30 PM - 03:30 PM
  Work on Projects
03:30 PM - 04:00 PM
  Tea
04:00 PM - 05:00 PM
  Formalizing Galois Theory
Thomas Browning (University of California, Berkeley)
Jun 15, 2023
Thursday
09:00 AM - 10:00 AM
  Polynomials and Algebraic Number Theory
Thomas Browning (University of California, Berkeley)
10:00 AM - 12:00 PM
  Work on Projects
12:00 PM - 01:30 PM
  Lunch
01:30 PM - 02:30 PM
  The Lean Simplifier and Other Automation
Jeremy Avigad (Carnegie Mellon University)
02:30 PM - 03:30 PM
  Work on Projects
03:30 PM - 04:00 PM
  Tea
04:00 PM - 05:00 PM
  Formalizing Blockchain Computations
Jeremy Avigad (Carnegie Mellon University)
Jun 16, 2023
Friday
09:00 AM - 10:00 AM
  Integration and Complex Analysis
Heather Macbeth (Fordham University at Lincoln Center)
10:00 AM - 12:00 PM
  Work on Projects
12:00 PM - 01:30 PM
  Lunch
01:30 PM - 02:30 PM
  Formalizing Sphere Eversion
Patrick Massot (Université Paris-Saclay)
03:30 PM - 04:00 PM
  Tea
04:00 PM - 05:00 PM
  Presentation and Discussion of Projects
Back to Summer Graduate School