Lean for Scientists and Engineers, Summer 2024 - Lecture 4

Lecture 4 of Lean for Scientists and Engineers course at University of Maryland, Baltimore County and online in Summer 2024.
This lecture covers more logical operators, including "not," "exists," "for all," "implication," and "if and only if." Examples from chemistry and physics are highlighted. The concept of "proportional to" used in various empirical scientific relationships can be represented formally using "exists" and "for all."
More content on proofs with intermediate steps, equalities, and inequalities can be found in Heather Macbeth's textbook, Mechanics of Proof: hrmacbeth.gith...
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