Proofs and Programs 2023 #

This course will introduce Lean Theorem Prover 4, which is an interactive theorem prover as well as a programming language and use it for various aspects of proofs and programs:

To study these things in a meaningful way, we will look at foundations of mathematics and of computation. We will introduce different foundational systems:

To browse the code, expand the PnP2023 tab on the left.

  • hello = "to the course Proofs and Programs"
Instances For