Lean and Computational Theorem Solving in Mathematics and Elsewhere

Thumbnail
Name:
6376_Joshua_Orton.pdf
Size:
265.6Kb
Format:
PDF
Download
Cast your vote
 
Your vote was cast
Thank you for your feedback
Author
Orton, Joshua S.
Keyword
First Reader Athar Abdul-Quader
Senior Project
Semester Spring 2023
Readers/Advisors
Abdul-Quader, Athar
Term and Year
Spring 2023
Date Published
2023

Metadata
Show full item record
URI
http://hdl.handle.net/20.500.12648/11759
Abstract
In this paper, I intend to demonstrate the use of the Lean theorem prover, applying it to a series of mathematical definitions and theorems, as well as discussing its applications in certain non-mathematical arenas. I will discuss and utilize the mechanisms of the language, demonstrate various capabilities of the theorem prover's language, and present definitions regarding the sets of natural numbers, integers, rationals and reals, and the quality of primeness, as well as the nature of lists, and a proof of the infinitude of primes, weaving in some speculation on the epistemological applications of this new language.
Accessibility Statement
Purchase College - State University of New York (PC) is committed to ensuring that people with disabilities have an opportunity equal to that of their nondisabled peers to participate in the College’s programs, benefits, and services, including those delivered through electronic and information technology. If you encounter an access barrier with a specific item and have a remediation request, please contact lib.ir@purchase.edu.
Collections