The goal was to translate a mathematical theory of order in the Lean theorem prover and check with Lean that various theorems can be proved using intuitionistic logic.
Skills and deliverables: Mathematics, Mathematical Modeling, Algorithm Development, Lean Theorem Prover, Formalization