Theorem proving in LEAN

Faculty Member

Philipp Hieronymi

Project Image

This project studies the proof assistant Lean (https://leanprover.github.io/) developed by Microsoft Research.
Formal verification and the use of proof assistants has increased substantially over last few years, in particular in the hardware industry. The goal of this project is to learn how to use Lean to verify basic mathematical proofs. We focus on proofs in model theory and o-minimality.
 

Team Meetings

Weekly

Project Difficulty

Intermediate

Undergrad Prerequisites

MATH 347 is required. Knowledge of basic type theory and logic will be helpful. Coding experience highly desired. We are looking for students who are able to install LEAN (https://leanprover.github.io/) by themselves, but we do not expect you to have actually worked with LEAN before. But if you have already worked with LEAN, please let us know in your application.