Lean Theorem Prover: The Lean, Mean, Math-Proving Machine

Authors

Presenter(s)

Ethan Shade, Sarah Herr, Kailey Peppard, Joseph Kopp

Comments

Presentation: 3:00-4:15 p.m., Kennedy Union Ballroom

Files

Description

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.

Publication Date

4-19-2023

Project Designation

Course Project 202310 MTH 342 01

Primary Advisor

Jun Li

Primary Advisor's Department

Mathematics

Keywords

Stander Symposium, College of Arts and Sciences

Institutional Learning Goals

Scholarship

Recommended Citation

"Lean Theorem Prover: The Lean, Mean, Math-Proving Machine" (2023). Stander Symposium Projects. 3081.
https://ecommons.udayton.edu/stander_posters/3081