(In)formalized Mathematics

Date:

I gave this talk for the McMaster Casual Math Seminar, in the Winter semester of 2024. The goal was to introduce graduate students and undergrads to the Lean 4 theorem prover.