Final Project Gallery

Formalizing TEAL (2025)

Franklin Harding

TEAL is a stack-based scripting language for the Algorand blockchain. This project is a very partial formalization of the language. The main proofs are 1). determinism of the modeled operations; and 2). a proof of correctness and cost for a very simple program. One of the interesting challenges of formalizing the language was dealing with hashing, and there are many more things I didn't get to like storage, transactions, and security proofs which would be interesting to work on.

1993 IMO Question 3 (2025)

John Rathgeber

A formalization of Question 3 from the 1998 IMO. The question gives a function d(n) that counts the number of divisors of n, and asks us to determine which integers can be written as d(n^2)/d(n) for some n. This project first proves mathematically that every odd number and only odd numbers satisfy this ratio, and then formalizes the proof in Lean.

A tactic for normalizing expressions in Fin n (2025)

Justus Adam

LEAN 4 Tactic for normalize equalities for expression that add and subtract `Fin n` values. Cancels repeating variables and sums constants. Applicable to hypotheses and goals, similar to `simp`. Uses a reflection style implementation.

Soundness and completeness of propositional intuitionistic logic (2025)

Feiyang Wang

I defined and proved the soundness and completeness of propositional intuitionistic logic via Hyting Algebra and Natural deduction. Several other systems are defined as well, and proved equivalence between them and ND.

2014 IMO Problem 1 (2025)

An Cao

This project formally verifies the solution to Problem 1 of the International Mathematical Olympiad (IMO) 2014 using Lean. It contributes to the collection of formalized Olympiad problems, which serves as a critical benchmark for automated theorem provers.

Axiomatic Set Theory (2024)

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 (2024)

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 (2024)

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 (2024)

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 (2024)

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 (2024)

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 (2024)

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 (2024)

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 (2024)

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 (2024)

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 (2024)

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 (2024)

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.