> ./projects --select "Lean 4"
Algebraic Logic & Topology
B.S. Thesis: Formalization
This project involves the formal verification of my Undergraduate Thesis in Mathematics, titled "Dualities for bounded distributive lattices with normal operators". The goal is to fully formalize the construction of Priestley Spaces and their duality with Distributive Lattices using the Lean 4 theorem prover.
> ./theorems --list-verified
- Priestley Duality Formal construction of the category of Priestley Spaces and its equivalence to Distributive Lattices.
- Canonical Extensions Proof of existence of canonical extensions for bounded distributive lattices with monotone operators.
This work is part of a larger effort to digitize 20th-century order theory results, making them accessible to AI-driven proof search algorithms.