Lean Proof Formalisation
This project was part of my dissertation at the University of Bath. The goal was to bring a proof from asymptotic analysis and ‘formalise’ it within the Lean proof assistant language.
Background
Proof assistants are software systems that help construct and verify mathematical proofs. Lean is one such language that relies on sophisticated type theory to check if proofs are valid. During my final semester, I studied the underlying logic and semantics of such languages, which helped make sense of the complicated type theory that Lean depends upon.
Work Completed
- Translated asymptotic analysis proofs into formal Lean code
- Studied the type theory underpinning the Lean proof assistant
- Verified proofs using Lean’s automated checking system
Image: Lean code example - 600x400
Related Topics
- Type Theory
- Formal Methods
- Mathematical Logic