Applied Math Colloquium: Tyler Josephson (UMBC)

Title: Formalizing Theorems in Mathematics and Theories in Science and Engineering

Abstract: Lean is an interactive theorem prover for writing and verifying mathematical proofs with computational logic. By systematically defining mathematical objects and proving theorems about them, mathematicians have used Lean to formalize >100k theorems across undergraduate and graduate mathematics, grounding all of them, axiomatically, in dependent type theory. Lean is even formalizing results from modern math research, including perfectoid spaces, the subject of the 2018 Fields Medal. The international Lean community is working to formalize the entirety of the undergraduate math curriculum, so Lean "knows" all math that a student with a B.S. in mathematics has learned.

In this talk, I will introduce the Lean theorem prover through a short demonstration and highlight opportunities for mathematicians to get involved in expanding Lean's math library. I will also share how Lean is being used in the classroom to teach proofs to undergraduates. Finally, I will share work from the AI & Theory-Oriented Molecular Science (ATOMS) Lab at UMBC exploring Lean for formally describing theories in science and engineering.

Prof. Josephson is from Chemical, Biochemical, and Environmental Engineering

There will be a tea and coffee hour from 10am in M&P 422.