Lean for Scientists and Engineers, Summer 2024 - Lecture 8

Lecture 8 of Lean for Scientists and Engineers course at University of Maryland, Baltimore County and online in Summer 2024.
Computations happen with floating point numbers, but it's hard to prove anything about them, especially when super-basic things like (a + b - b = a) don't hold for floating point numbers. But real numbers (on which calculus, trigonometry, etc. are built) are non computable. We proposed to bridge these using polymorphic functions, the main topic of this lecture. We also start discussing lists and arrays.
Functional Programming in Lean:
lean-lang.org/...
Course content is available on GitHub, including slides and Lean code: github.com/ATO...
Huge thanks to the National Science Foundation! This work was made possible by NSF CAREER Award 2236769