Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
import PnP2023.Lec_01_04.Intro
import PnP2023.Lec_01_04.OddExample
import PnP2023.Lec_01_06.NatEq
import PnP2023.Lec_01_11.NatLe
import PnP2023.Lec_01_13.NatRec
import PnP2023.Lec_01_18.NatSub
import PnP2023.Lec_01_20.NatMin
import PnP2023.Lec_01_20.NatMinus
import PnP2023.Lec_01_25.Answer
import PnP2023.Lec_02_01.Foundations
import PnP2023.Lec_02_03.InductiveTypes
import PnP2023.Lec_02_15.PropsAsTypes
import PnP2023.Lec_03_01.RandomIO
import PnP2023.Lec_03_08.Diaphontine
import PnP2023.Lec_03_10.FormalCalculus
import PnP2023.Lec_03_24.Sampling
# Proofs and Programs 2023

This course will introduce [Lean Theorem Prover 4](https://leanprover.github.io/), 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.


hello: String
"to the course Proofs and Programs": String
"to the course Proofs and Programs"