Logo

Mathematical Sciences Research Institute

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
  Lecture and Discussion
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
  A Tour of Community Resources
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 - 02:15 PM
  Sets and Functions (Chapter 4 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
  Basics of Type Theory Foundations
Jun 07, 2023
Wednesday
09:00 AM - 10:00 AM
  Number Theory (Chapter 5 of MIL)
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
  What Meta-Programming Means and Looks Like
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 - 02:15 PM
  Lecture and Discussion
02:15 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
Jun 09, 2023
Friday
09:00 AM - 10:00 AM
  Topology (Chapter 7 of MIL)
10:00 AM - 12:00 PM
  Exercise Session
12:00 PM - 01:30 PM
  Lunch
01:30 PM - 02:15 PM
  Lecture and Discussion
02:15 PM - 03:30 PM
  Exercise Session
03:30 PM - 04:00 PM
  Tea
04:00 PM - 05:00 PM
  Presentation of Possible Projects for Week 2
Jun 12, 2023
Monday
09:00 AM - 10:00 AM
  Commutative Algebra and Linear Algebra
10:00 AM - 12:00 PM
  Exercise Session
12:00 PM - 01:30 PM
  Lunch
01:30 PM - 02:15 PM
  Calculus and Integration (Chapters 8 and 9 of MIL)
02:15 PM - 03:30 PM
  Exercise Session
03:30 PM - 04:00 PM
  Tea
04:00 PM - 05:00 PM
  Definitions and Theory Building
Jun 13, 2023
Tuesday
09:00 AM - 10:00 AM
  Category Theory
10:00 AM - 12:00 PM
  Exercise Session
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
Jun 14, 2023
Wednesday
09:00 AM - 11:00 AM
  Work on Projects
11:00 AM - 12:00 PM
  First Progress Report on Projects, Discussion
12:00 PM - 01:30 PM
  Lunch
01:30 PM - 02:15 PM
  Lecture on Topics Related to Projects
02:15 PM - 03:30 PM
  Work on Projects
03:30 PM - 04:00 PM
  Tea
04:00 PM - 05:00 PM
  Formalizing Cohomology
Jun 15, 2023
Thursday
09:00 AM - 10:00 AM
  Lecture on Topics Related to Projects
10:00 AM - 12:00 PM
  Work on Projects
12:00 PM - 01:30 PM
  Lunch
01:30 PM - 02:15 PM
  Lecture on Topics Related to Projects
02:15 PM - 03:30 PM
  Work on Projects
03:30 PM - 04:00 PM
  Tea
04:00 PM - 05:00 PM
  Formalizing Sphere Eversion
Jun 16, 2023
Friday
09:00 AM - 10:00 AM
  Lecture on Topics Related to Projects
10:00 AM - 12:00 PM
  Work on Projects
12:00 PM - 01:30 PM
  Lunch
01:30 PM - 03:30 PM
  Presentation and Discussion of Projects
03:30 PM - 04:00 PM
  Tea
04:00 PM - 05:00 PM
  Presentation and Discussion of Projects
Back to Summer Graduate School