FAA 2025 Class Projects

Formalization of Analysis of Algorithms - ETH Zurich

Quick Start

git clone https://github.com/sorrachai/FAA2025_class_projects.git
cd FAA2025_class_projects
lake exe cache get
lake build

Workflow

Create your branch

git checkout -b project1-yourname

Work on your project

Create a new folder named after your last name. Edit files in Projects/[LastName]/

Test locally

lake build

Submit

git add .
git commit -m "Complete Project 1"
git push origin project1-yourname

Then create a Pull Request on GitHub.

CI Checks

Automatic checks on every push:

• Build: Must compile successfully
• Sorry count: Number of incomplete proofs
• Axiom usage: Custom axioms are not allowed
• Linter: Code quality warnings

Resources

• Lean 4 Documentation
• Theorem Proving in Lean 4
• Mathlib Docs