Presenter(s)

    Ethan Shade, Sarah Herr, Kailey Peppard, Joseph Kopp

    Comments

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

    Download

    Download Project (254 KB)

    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

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

    Share

    COinS