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 Wibowo

This 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 Zhao

Linearly 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 Kermorgant

In 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 Gupta

A 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 Agvanian

We 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 Oak

This 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 Kashyap

SAT 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 Advani

This 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 Jung

A 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 Li

This work uses Lean4 to define and make proofs on Deterministic Finite Automaton Minimization, including partitioning states and removing unreachable states.

Domain Theory Formalization

Zekai Li

This project formalized the way-below relation, the continuous directed-complete partial order and some useful theorems in domain theory

Linear Algebra Done More Right

Laura Romig

My final project is a formalization of part of the first chapter of *Linear Algebra Done Right* by Sheldon Axler. The chapter starts with defining and proving properties about Complex numbers, then moves to defining sets of equal-length lists (Fn) and proving things about these, and then uses these together to motivate the definition of vector spaces, which the book uses as the foundation of teaching Linear Algebra.