Loading...
Thumbnail Image
Publication

Lean and Computational Theorem Solving in Mathematics and Elsewhere

Journal Title
Readers/Advisors
Abdul-Quader, Athar
Journal Title
Term and Year
Spring 2023
Publication Date
2023
Book Title
Publication Volume
Publication Issue
Publication Begin
Publication End
Number of pages
Research Projects
Organizational Units
Journal Issue
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.
Citation
DOI
Description
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.
Embedded videos