Nijholt, Jard (2025) Computer-assisted proofs in LEAN4. Bachelor's Thesis, Mathematics.
|
Text
bMATH2025NijholtJ.pdf Download (584kB) | Preview |
|
![[img]](https://fse.studenttheses.ub.rug.nl/style/images/fileicons/text.png) |
Text
Toestemming.pdf Restricted to Registered users only Download (177kB) |
Abstract
This thesis explores the use of the proof assistant LEAN4 in the formalization and verification of mathematical proofs. Proof assistants enable mathematicians to express proofs in a fully formal language that can be checked by a computer, ensuring complete logical rigor and eliminating the ambiguities of informal reasoning. We first discuss the theoretical foundations behind LEAN4. This includes the Calculus of Inductive Constructions and the Curry-Howard correspondence. We show how LEAN4 works in practice. We explain common tactics to use in LEAN4, as well as pitfalls that arise as we formalize our proofs. To illustrate the power of LEAN4, we look at the PhysLean library, and discuss some contributions made to this library. Finally, we show the reader how to get involved; we touch upon several open-source projects and educational resources to help readers get involved into the LEAN4 community.
| Item Type: | Thesis (Bachelor's Thesis) |
|---|---|
| Supervisor name: | Seri, M. and Sterk, A.E. |
| Degree programme: | Mathematics |
| Thesis type: | Bachelor's Thesis |
| Language: | English |
| Date Deposited: | 07 Nov 2025 15:05 |
| Last Modified: | 07 Nov 2025 15:05 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/37126 |
Actions (login required)
 |
View Item |