Functional Programming and Theorem Proving in Lean 4

Catalog description

Objectives: Historically, mathematics and reasoning has almost always been done in prose: natural language text describing the relevant steps and logic involved. With the help of Proof Assistants, computers can automatically check mathematical proofs and reasoning. In this course we will give an introduction to Lean 4, a proof assistant and purely functional programming language. We introduce Lean first as a programming language for the first half of the course. In the latter half of the course, we explain its proof assistant features. Topics: Abstract data types, monads, error handling, type instances, type theory, specifically the calculus of inductive constructions (CIC), expression- and tactic-based theorem proving, and various libraries in Mathlib4. Target Audience: Students who want to learn about formalizing mathematics are the primary audience. The goal of the course is not to learn advanced mathematical concepts since the mathematical part stops at differential calculus. Students only need a reasonable aptitude in mathematics as a prerequisite. The secondary audience are researchers