Final Projects

Overview

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, a mathematical theorem, a system property, or a protocol invariant. 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 Lean4’s standard library, Mathlib, and the tactics they offer. 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 below. You’re welcome to pick one of these or to propose your own.

Project Requirements

There are very few formal requirements for these projects, since we want to give you the freedom to work on whatever you like. We ask only that:

Core Requirements

1. Prove some theorems!
   A project ideally shouldn’t be fully computation/modeling. You must formally verify at least one meaningful property about your system/algorithm/structure.

2. Write a README
   Your README should explain:

   • High-level overview of your project (“Overview”)
   • Why you defined things the way you did (“Design choices”)
   • What properties you proved and why they matter (“Main theorems”)
   • Explain your approach to key proofs (“Proof strategies”)
   • What was difficult and how you overcame it (“Challenges”)

3. Submit Working Code
   All .lean files must compile without errors. Include clear comments throughout your code.

4. Present Your Work
   Prepare a 5 minute presentation for Week 10 that demonstrates your verification and explains your key insights.

Timeline

Week 9 (Project Kickoff)

• Start thinking about possible project ideas
• Attend the brainstorming session
• Submit project proposal within 3 days

Weeks 9-10 (Development)

• Implement your formalization
• Prove your theorems
• Write your documentation
• Prepare your presentation

Week 10 (Final Session)

• Project due at presentation time
• Present your work (3-5 minutes)
• Submit all materials before presenting

Project Ideas

For your sake, projects must be small enough to be “provable” in approximately 2 weeks. You are free, however, to voluntarily work on a larger project, which will (of course) be rewarded. Here are some project ideas organized by background, but feel free to propose your own!

Note on Mathlib Contributions: Some students may choose to contribute to Mathlib or CSlib as their final project. If you’re interested in this path, Rida Hamadani is available to review and provide guidance on Mathlib-related or CSlib-related projects. This is entirely optional but offers a unique opportunity to contribute to the broader Lean mathematical library.

Computer Science Projects

TBD

Mathematics Projects

TBD

Engineering Projects (ECE/CCE)

TBD

Interdisciplinary Projects

TBD

Proposing Your Own Project

Once you settle on one project you want to work on, you must write an informative project proposal to be sent to the course team.

Write a Proposal

Your proposal (written in LaTeX) should include:

• Title: Clear, descriptive name
• Overview: What will you verify? (2-3 sentences)
• Core Property: The main theorem you’ll prove
• Challenges: Anticipated difficulties

Consult Course Staff

Discuss your proposal via email or Discord.

Project Evaluation Criteria

• Technical Content (50%): Correctness of definitions, quality of specifications, soundness of proofs
• Documentation (25%): Clear README, well-commented code, explanation of proof strategies
• Presentation (15%): Clear explanation, demonstration, time management
• Creativity (10%): Novel approach, going beyond course material

Resources

• Theorem Proving in Lean 4
• Functional Programming in Lean 4
• Mathlib Documentation
• Course Discord Server

Submission Checklist

• All .lean files compile without errors
• README.md is complete
• Code is properly commented
• Presentation prepared
• Submitted a public or private GitHub repository containing the Lean project

FAQ

Can I work in a pair? Yes! This is not recommended, but if you will work in pairs, make sure to clearly divide responsibilities and both be present.

Can I use online resources? Yes, but cite sources and core proofs must be your own.

What if I get stuck? Document what you attempted and where you got stuck. Partial progress is valuable.

Navigation

← Back to Course Overview
Week 9: Project Kickoff →

Questions? Reach out on the course Discord!