leetproof.org is a platform for theorem proving practice in Lean 4. LeetCode, but for formal proofs.
- Problems — A growing library of proof problems across math and computer science. Each problem is meant to teach something distinct.
- Built-in editor — Solve problems directly in the browser with an embedded Lean 4 editor and live feedback.
- Solutions — Solve a problem, then browse others solutions to discover new approaches and write more concise proofs. Example: solutions for collatz-terminates.
- Hint packs — Hint packs provide step-by-step guidance for problems, ranging from a high-level suggestion to a one-click code completion, without simply revealing the full solution. Example: hints for list-reverse-reverse.
- Sign in — Sign in with Google to save submissions and share solutions and hint packs with the community.
- Free & open source — All features are free.
Problems live as markdown files in problems/. Pull requests are welcome. Contributors should avoid problems that mainly reteach the same concept as an existing one.
Instructions for running LeetProof locally or contributing code are available in TECHNICAL.md.