The inaugural UW Lean Hackathon brought together students, faculty, and industry partners to build 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.
Stay tuned for more in 2027.
theorem Nat.zero_add : ∀ n, 0 + n = n
| 0 => rfl
| n + 1 => congrArg Nat.succ (Nat.zero_add n)The inaugural UW Lean Hackathon has concluded. These projects were recognized by the judges for their novelty, technical execution, and community impact!
A category-theoretic rewrite tactic for Lean 4.
Brings category-theoretic rewriting to Lean 4 with `cat_rw`, letting users rewrite objects, goals, and propositions using isomorphisms.
Leopold Mayer • Grant Yang • Brian Nugent
Neural-guided automated proof search for Lean 4.
Adds learned guidance to Lean 4 tactics like `grind` and `aesop`, combining neural branching heuristics with tooling for collecting and training on proof search data.
Theo Meek • Simon Chess • Evan Wang • Sophie Szeto
A repository for Lean 4 formalizations outside mathlib’s scope.
Collects Lean 4 formalizations outside mathlib’s scope, with a workflow for discovering projects, checking them automatically, and promoting accepted work into a shared library.
Vasily Ilin • Justin Asher
Recognized by the judges for standout work.
Nels Martin • Sukhman Singh • Tanish Vaidya
Evan Gubarev • Tim Avilov
Kieran Rullman • John Ye • Nicholas Mundy • Owen Parks
theorem winner_showcase :
first ∧ second ∧ third := by
repeat constructorThanks to our special guests for sharing their expertise, and to our judges for helping make the inaugural UW Lean Hackathon possible.
Creator of Lean. He spoke on machine-checked mathematics, AI collaboration, proof automation, and the role of Lean as long-term open infrastructure for verified software and mathematics.
Supported teams throughout the event, drawing on his experience as a maintainer of mathlib and helping participants navigate formalization work in Lean.
With thanks to the panel who evaluated projects and selected this year’s winners.
Supporting advances in formal verification and proof automation.
Sponsordef fibonacci : ℕ → ℕ
| 0 => 0
| 1 => 1
| n + 2 => fibonacci n + fibonacci (n + 1)The 2026 hackathon has concluded. We’re excited to build on this year’s projects, community, and collaborations when UW Lean Hackathon returns in 2027.
An invitation-only event at the intersection of mathematics, programming languages, and AI — hosted at the University of Washington.
Formalize mathematical statements and their proofs in Lean with the goal of contributing to Mathlib.
Create and improve infrastructure and tools that assist the formalization process.
Foster collaboration across PL, verification, LLMs, and mathematics communities.
Introduce Lean to a wider audience and grow the ecosystem of contributors and users.
Build and deepen connections between academia and industry around formal verification.
Tackle ambitious cross-disciplinary projects that push the boundaries of what's possible.
import Mathlib.Data.Nat.Prime.Basic
#check Nat.Prime
-- ℕ → Prop