Day/Date/Time: Thursday January 18, 4:30 – 5:30 pm
Speaker: John Nicholson
Title: “(In)formalized Mathematics: An introduction to the Lean theorem prover”.
Abstract: Computer proof assistants have recently gained traction in mainstream mathematical discourse. In this talk, we will delve into the concepts behind computer proof assistants, briefly survey the various proof assistants to choose from, and discuss some ongoing projects in the formalization of mathematics. We will conclude by proving some elementary results in Lean.
Coffee available beforehand at 4pm in Hamilton Hall 216 (Lounge).
