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 you:

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
• Submit project proposal: deadline is 25 March

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.

Easy Project Ideas

• Verified Sorting Algorithms: Formalize a basic sorting algorithm (e.g., Insertion Sort or Selection Sort). Define a Sorted inductive predicate and a Permutation predicate. The final theorem will prove that the output is both sorted and a valid permutation of the input list.
• Fundamental Number Theory: Implement the (extended) Euclidean algorithm for computing the greatest common divisor (GCD) and formally verify its correctness, eventually working your way up to proving a basic version of Bézout’s identity or the infinitude of primes.
• Expression Evaluation and Optimization: Define an Abstract Syntax Tree (AST) for simple arithmetic expressions (addition, multiplication, constants). Write a simplification pass (like constant folding, e.g., turning 0+x into x) and prove that evaluating the optimized AST always yields the same result as the original.

Intermediate Project Ideas

• Verified Stack Machine Compiler: Define a simple stack-based machine (with instructions like PUSH, ADD, MUL) and write a compiler that translates arithmetic ASTs into stack instructions. The capstone theorem proves compiler correctness: executing the compiled instructions on an empty stack yields the exact same integer as evaluating the original AST.
• Discrete Sequence Convolution: Formalize discrete-time sequences as functions from ℕ to ℝ (or ℤ). Define the discrete convolution sum and formally verify its algebraic properties, specifically commutativity and associativity.
• Verified Order Book: Model a simplified financial exchange order book using binary trees. Define structures for Bid and Ask orders, implement an insertion algorithm, and prove a critical market invariant: the highest bid in the tree is strictly less than the lowest ask, ensuring no crossed markets.

Difficult Project Ideas

• Group Theory and Lagrange’s Theorem: Define a Group type class (identity, inverse, associativity). Define what a Subgroup is, define left and right cosets, and prove that cosets partition the group. For an ambitious finish, prove Lagrange’s Theorem for finite groups.
• Balanced Search Trees (AVL or Red-Black): Implement a self-balancing tree. The challenge is defining the balancing invariant (e.g., the height difference between subtrees is at most 1) and proving that the tree rotations (left/right) preserve this invariant and maintain the binary search property.
• Rudimentary High-Assurance Cryptography (RSA or Diffie-Hellman Key Exchange): Formalize the mechanics of a public-key cryptosystem. Implement modular exponentiation and use Fermat’s Little Theorem to formally verify that encryption followed by decryption returns the original message.

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.

Proposing Your Own Project (Deadline: Sunday, 5 April)

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
• The Hitchhiker’s Guide to Logical Verification
• Mathematics in Lean
• Metaprogramming in Lean 4
• Mathlib Documentation
• Course Discord Server

Additional Online Resources

• Lean4 Documentation
• Mathlib Documentation
• Lean Zulip Chat
• Lean Community

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

Presentation (Deadline: Friday, 10 April)

To finalize your project submission, you are expected to present your work online on Friday, 10th of April, in front of the course team and other students. The presentation should be 5-7 minutes with an additional 2-3 minutes of time for questions. If you wish to request more time, contact the course organizers via email.

You will be evaluated based on the criteria listed above, as part of the PROOF101 final projects competition, with the top students in that competition being entitled to cool prizes!

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? Ask on the Discord server for help from the PROOF101 community, and 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!