# 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*:

- Using programs (
*interactive theorem provers*) to- verify proofs of results
- help in generating proofs

- Proving correctness of programs
- Writing programs to find and/or verify proofs
*Functional Programming*in Lean

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

*Dependent Type Theory*(DTT): foundations used by Lean that include both proofs and computations in a unified way.- Classical foundations:
*First-order logic:*the usual foundations of mathematics.*lambda-calculus:*one of the equivalent formulations of the usual foundations of computation.

## Navigation #

To browse the code, expand the `PnP2023`

tab on the left.