A hackathon bringing together students, faculty, and industry partners to work on projects showcasing the power of the Lean Proof Assistant. Projects span algorithm-driven proofs, pictorial reasoning, paper folding, games, data structures, and AI-driven autoformalization.
theorem Nat.zero_add : ∀ n, 0 + n = n
| 0 => rfl
| n + 1 => congrArg Nat.succ (Nat.zero_add n)Presentation of all projects.
Dinner to encourage folks to stay late and keep hacking!
Room will be available for those who want to continue.
Use these project ideas as inspiration. Feel free to pick from this list, but make sure to put in your own twist! Up-to-date as of April 1, 2026.
Write a tactic that can prove a given point is an optimal solution to a linear program (using duality).
Implement algorithms for graphs such as computing augmenting paths for matchings and flows. Prove that these paths really do augment the matching/flow in the appropriate way.
Formalize the Huzita–Hatori Axioms of Paper Folding in Lean and prove that they can be used to solve cubic equations. Build a tool to visualize the folds and verifiably compute the coordinates of points obtained through folds.
Make Sudoku in Lean. Write a solver for Sudoku in Lean. Prove the correctness of your solver.
Port a useful data structure to Lean and write useful theorems about it. For example, there are many variants of map data structures which may be useful. See lean-map for inspiration.
theorem inf_primes (n : ℕ) :
∃ p, n ≤ p ∧ Nat.Prime p :=
Nat.exists_infinite_primes n#check @List.map
-- {α β : Type} →
-- (α → β) → List α → List βSupporting advances in formal verification and proof automation.
Sponsordef fibonacci : ℕ → ℕ
| 0 => 0
| 1 => 1
| n + 2 => fibonacci n + fibonacci (n + 1)Apply to join us May 8–10, 2026 at the University of Washington for two days of hacking, learning, and collaboration around the Lean Proof Assistant. Spaces are limited — applications will be reviewed by the organizing committee.