Formalizing Mathematics in Lean

About

An interactive theorem prover is a computer program to assist with the development of mathematical proofs. By checking and automating proof steps, the machine aides the user in creating proofs in a formal language understandable to the program.

Formalizing mathematics is the process of typing mathematical proofs into the interface of an interactive theorem prover. In the past years, more and more mathematics, from undergraduate level to the frontiers of modern research have been formalized in a variety of proof assistants.

While there are many interactive theorem provers, this course focuses on Lean and its mathematical library mathlib, which already contains a substantial number of proofs of mathematical theorems and infrastructure for proof automation.

Course leader

Dr. Johan Commelin

Fee info