How would you like to, not just find and correct bugs in your code, but write code that’s provably free of bugs? How can rigorous, computer-checked logic be used in science, engineering, and AI?
Lean 4 is a programming language whose type system enables it to check complicated math proofs. This ~22-hour lecture series is an introduction to Lean for non-mathematicians (we recommend a prerequisite of Calculus II). This was taught at the University of Maryland, Baltimore County and online in Summer 2024.
Topics include:
- Logic and proofs for scientists and engineers
- Functional programming in Lean 4
- Provably-correct programs for scientific computing
Lecture recordings are now on YouTube!
The Lean code in this repository was compatible with the versions of Lean and Mathlib that were current in August 2024. To try the code with the latest versions of Lean and Mathlib, try the Lean Language Server.
Thanks to Tomas Skrivan, our guest speaker for Lecture 11 (the code for his repo is here)! Also, thanks to ATOMS Lab members Ejike (David) Ugwuanyi, Colin Jones, Alan Vithayathil, Oscar Matemb, and Shashane Anderson for contributing to course content, developing example problems, and editing lecture recordings.
Also, big thanks to Heather Macbeth for writing Mechanics of Proof and to David Thrane Christiansen for writing Functional Programming in Lean.
This work was made possible with funding from the National Science Foundation, NSF CAREER Award 2236769