LeetProof
Prove theorems in Lean 4, share your solutions, and sharpen your formal verification skills.
What is LeetProof?
LeetProof is a collaborative platform focused on formal verification using the Lean 4 programming language. Instead of writing algorithms, you write mathematical proofs and verified programs.
1. Pick a Problem
Browse problems by difficulty — easy, medium, or hard. Each problem describes a theorem to prove or code to verify in Lean 4.
2. Write Your Proof
Use the built-in code editor right in your browser — no install required. Get real-time feedback, goal states, and error messages as you construct your proof.
3. Verify & Submit
When Lean's type checker accepts your proof with no errors, you've solved it! Track your progress and compare with other users.
4. Learn & Share
Browse others' solutions for different approaches, or unlock progressive hint packswhen you're stuck — without spoiling the full proof.
Problem Categories
Logic & Propositional
And, Or, Implies, Not, classical reasoning, type theory
Algebra & Number Theory
Natural numbers, arithmetic
Data Structures & Functions
Lists, Strings, Trees, higher-order functions
Math Puzzles & Games
Logic puzzles, game theory, combinatorics
Set Theory & Geometry
Set equalities, geometric reasoning
Program Verification
Correctness proofs for algorithms and programs
Ready to prove something?
Sign in with Google to save submissions and share solutions and hint packs with the community — it's free.
LeetProof is free and open source.