Final Project Gallery
Collection of amazing projects created as part of the final for Formal Proof and Verification. Use for inspiration and click to see the full source code!
Axiomatic Set Theory
Edward WibowoThis project seeks to formalize an axiomatic approach to set theory within Lean. Drawing inspiration from Enderton's Elements of Set Theory, it begins with the fundamental axioms and proceeds to formalize selected theorems and exercises presented in the book. Definitions and theorems build up from fundamental axioms to relations, functions, and natural numbers.
Formalizing Linearly Typed Lambda Calculus
Gavin ZhaoLinearly Typed Lambda Calculus (LTLC) builds on top of the Simply Typed Lambda Calculus (STLC) we learned in class by adding linear types. That is, we impose a restriction that every variable must be used EXACTLY once. Similar ideas are used in languages like Rust to ensure memory safety and prevent memory leaks. We first formalize the syntax and semantics of LTLC, and then prove that it abides by the progress theorem and the preservation theorem.
Dedekind cuts: The real way to define the Reals
Mathilde KermorgantIn 1872, Dedekind and Cantor both proposed the first constructions of the Real numbers. Cantor used Cauchy sequences, while Dedekind proposed something called Dedekind cuts. This repository contains a formalization for Dedekind cuts, with the goal of proving that they form a commutative ring. We define addition, negation, and multiplication and prove important properties about these operations. Distributivity and associativity of multiplication are left as an exercise to the reader.
Free Will Lean
Vedant GuptaA formal proof of the Kochen-Specker paradox using Lean 4 and Mathlib. Informally, the paradox shows the impossibility of predetermined/deterministic experiment outcomes for certain particles, setting up the foundation for Kochen and Conway's Strong Free Will theorem.
Verifying the correctness of a k-anonymity implementation in Rust
Artem AgvanianWe verify the correctness of a simple k-anonymity implementation in Rust using Aeneas. Aeneas is a compiler that translates Rust code to a variety of proof assistant backends like Lean, Coq, and others. We use Lean as a backend of choice and encode the specification for the implementation.
FormalML: Formalizing machine learning concepts in Lean
Prithvi OakThis project aims formalize some of the most fundamental concepts and ideas in Machine Learning, including classifiers, hypothesis classes, and VC dimension. With the ongoing push for "Explainable AI", formalizing ML concepts is a relevant potential solution.
Verified SAT Solver
Karan KashyapSAT solvers are increasingly being used to power "automated reasoning" systems. Given the critical nature of some applications of these tools, it seems important to verify the correctness of the SAT solvers we use. This project is an implementation of a DPLL SAT solver in Lean. It also includes some proofs about the correctness of the SAT/UNSAT results returned by the solver.
A Dice Probability Problem
Anand AdvaniThis project sets up a sample space for the roll of a fair die and a uniform probability distribution on that sample space. A couple basic things about this sample space are proved, and the project sets up the sketch of a proof that the expected value of the number of rolls of a fair die until a 6 is rolled equals 6.
Verified Lua Tables
Seong-Heon JungA model of Lua 5.0's table (hashmap, dictionary) implementation. The model proves the non-collision property of the table, where a collision in the table occurs only if two items share the exact same "main" value (i.e. hash)
Deterministic Finite Automaton Minimization
Zekun LiThis work uses Lean4 to define and make proofs on Deterministic Finite Automaton Minimization, including partitioning states and removing unreachable states.
Domain Theory Formalization
Zekai LiThis project formalized the way-below relation, the continuous directed-complete partial order and some useful theorems in domain theory