Proofs and Programs 2025

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

Navigation

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