← Mathematics & Modelling
Formal Verification in Lean 4
Master's thesis work formalizing mathematical proofs using the Lean 4 theorem prover, focusing on directed acyclic graphs and divisibility.
Overview
My master’s thesis involves formalizing mathematical concepts in Lean 4, a dependently typed programming language and interactive theorem prover. The project focuses on proving properties of directed acyclic graphs and division algorithms.
What is Formal Verification?
Unlike traditional mathematical proofs written in natural language, formal proofs are checked by a computer. Every logical step must be explicitly justified, making errors impossible. Lean 4 provides both the language to express these proofs and the engine to verify them.
Key Contributions
- Formalized DAG properties and operations in Lean 4’s type system
- Proved termination of division algorithms using well-founded recursion
- Developed reusable tactics for common proof patterns in graph theory