- Students may submit assignments one or two days late, up to a total of six late days over the semester. For example, you could be one day late on six different assignments; two days late on three different assignments; or any combination in between. If longer extensions are needed in exceptional circumstances, please contact the instructor directly.
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.
We suggest that you start thinking about possible project ideas as early as possible. As the course goes on, we’ll 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 December 15 at 11:59pm. You’re strongly encouraged to talk to Rob and the TA staff before then to get early feedback.
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.
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).
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
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!
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
element_of : 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.