Notes

Notes will be posted occasionally to supplement the material in lectures and references.

• Overview

  Wednesday, Jan 4, 2023.

  About the course

  Here we sketch the what, the why, the how, and the why now of this course.

Read more…

• Foundations

  Tuesday, Jan 31, 2023.

  Foundations We have seen all the ingredients of the foundations of mathematics as implemented in Lean. Our goal now is to: Systematically review them. Put them in the context of what we mean by foundations of mathematics. Separate the foundations from the syntax parsing and elaboration which help us work efficiently with Lean. Foundations of foundations The starting assumption is that we are in agreement with the meaning of syntax, including pattern matching and substitution.

Read more…