Ethan Shade, Sarah Herr, Kailey Peppard, Joseph Kopp
Download Project (254 KB)
This is an exploratory project for MTH 342 - Set Theory. Lean Theorem Prover is a computer programming language that allows for the formalization of mathematical proofs and the use of computer-readable logic. We explore the structure and syntax of Lean and show how this can be used to formalize mathematical proofs. We identify classic math proofs that have already been formalized within Lean, as well as discuss how this language can advance the writing of proofs. Finally, we investigate proofs that are still yet to be formalized, and the potential reasons why they have yet to achieve formalization in Lean.
Course Project 202310 MTH 342 01
Primary Advisor's Department
Stander Symposium, College of Arts and Sciences
Institutional Learning Goals
"Lean Theorem Prover: The Lean, Mean, Math-Proving Machine" (2023). Stander Symposium Projects. 3081.