Final Project

The final project is your opportunity to apply what you’ve learned in this course. You will pick a topic and develop a formal theory about it: you’ll define the objects/programs, specify their behavior, and prove that these specifications hold. This topic can be an algorithm or a bit of math. The final result won’t necessarily be a lot of code – sometimes a lot of thought goes into a short verification!

A good project will go a bit beyond what we cover in this course. You’ll need to explore a bit of Lean’s standard library and the tactics that it offers. You’re welcome to import whatever library files you find useful.

You’ll consult with the course staff before starting on your project, to make sure the topic is manageable and in scope. We include some ideas here. You’re welcome to pick one of these or to propose your own.

For the most part, we expect these to be individual projects. It can be difficult to parallelize work on formalizations, since small changes to definitions or specifications can have far reaching effects. However, if you’re really excited about an idea that’s big enough for two people, come talk to Rob.

Project specs

There are very few formal requirements on these projects. I ask only that:

You may work on your project inside the fpv2024 repository/Lean project, or start a fresh project. We recommend the latter if you expect to have a bunch of files. It also makes it convenient for us to look at if you push your work to GitHub.

Dates

We suggest that you start thinking about possible project ideas as early as possible. As the course goes on, we may populate the list below with more suggestions.

By mid November, you should talk to Rob about what you might want to do.

The project is due on Monday, December 16. You’re strongly encouraged to talk to Rob and the TA staff before then to get early feedback.

Project suggestions

The one requirement is that you need to prove something! It’s not enough to only define some types and predicates.

Functional data structures and algorithms

Pick a familiar data type and associated operations, implement it in Lean, and verify some properties of these operations.

There are some good ideas in chapters 8 and 9 of the textbook Certified Programming with Dependent Types by Adam Chlipala: red-black trees, heterogeneous lists, and others. Non-dependent data types are okay too: you could even implement a few sorting algorithms and compare them. Graphs and graph algorithms can be good projects, e.g., Tarjan’s algorithm.

Or: pick a “competitive programming” problem, solve it, and prove that your solution is right. This statement of correctness could have many forms – it depends heavily on what the problem is. See the USACO problems for one source of inspiration.

Program semantics

Extend the toy WHILE language that we used in class with extra features. For example, give it static arrays, or function definitions, or multiple datatypes, or pointers/references. Sections 2.4 and 2.5 of Nielsen, et al have some great ideas! Then adjust the semantics. (What kind of semantics? Your choice.) Update the proofs of some of the properties we showed in class, or prove new properties that hold with your adjustment.

You could choose languages that aren’t based on WHILE. For example, you could implement simply typed lambda calculus, or a pure type system (see, e.g., Benjamin Pierce, Types and Programming Languages, which is available online with your Brown credentials).

Logic

Unsurprisingly, lots of people like to formalize logic in proof assistants! All of these involve defining the syntax of some logic, say, the type of propositional formulas.

You could implement a SAT solver and verify its correctness. (E.g., define an interpretation function Fmla -> Assn -> Bool, and show that if your solver returns SAT on a formula, there is an assignment for which it interprets to true.) Don’t necessarily aim for efficiency – simplicity is key.

You could also work on proof systems for first order logic: Gentzen’s sequent calculus, natural deduction, or tableaux methods would all make nice projects. Prove, e.g., the soundness and completeness of a particular method. Separation logic is a CS-focused logic with a different twist to it. Verifying properties of (some particular) modal logic would be interesting too.

Or, you could study some topic in the theory of first-order terms: matching algorithms, term rewriting, etc. This will be easier if you’ve taken a theory class on these topics of course!

Mathematics

The limits here depend on how far you want to dive into mathlib. Find some topic in a math class interesting? It’s possible to formalize it. (But we should be careful about the scope…) It’s always helpful to follow an (unformalized) textbook presentation for doing these things.

Abstract algebra is a place to start. Follow the beginning of an algebra textbook (without using too much from mathlib) to define some algebraic structures and prove the fundamental results about them.

Some basic graph theory/combinatorics can be interesting too. These topics are often discussed with a lot of informal intuition, so translating this to Lean can be a fun challenge.

You can embed axiomatic set theory in Lean! Declare two constants Set : Type and ElementOf : Set -> Set -> Prop, write down the axioms of set theory, and prove some fundamental results.

Prof. Hughes has taught a course at Brown about formalizing projective geometry in the proof assistant Isabelle. It would be interesting to begin adapting this to Lean. Prof. Hughes followed Hartshorne’s textbook; the very beginning of this textbook could make a nice, potentially tough, project.

IMO problems are a great source of interesting puzzles. Some are way out of scope, some are doable with nothing from mathlib, others are in between. There’s a big archive of problems online, and even some formalized in Lean already.

Metaprogramming

Because we talk about metaprogramming (tactic writing) at the very end of the semester, it can be a tough choice for a final project. But every once in a while someone works ahead and takes one on. One interesting (and useful!) idea: write a tactic that proves facts about partial orders. That is, it will prove things like the following:

α : Type
inst : PartialOrder α 
a b c d : α 
hab : a < b
hbc : b = c 
hdc : d ≥ c
⊢ a < d

On one hand, this is a lot simpler than linarith because it doesn't handle addition and scalar multiplication. On the other hand, it's more general, since it doesn't assume any algebraic structure or a linear order.

Some ideas from years past

For inspiration, here is a small selection of topics of projects from years past! Note that these range a lot in scope. This list is not comprehensive. Talk to the TAs about their projects and their experiences!