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 12. You’re strongly encouraged to talk to Rob and the TA staff before then to get early feedback.

Project suggestions

Coming soon!