LeetLean
Competitive theorem proving in Lean 4. Prove complex theorems, verify code, and sharpen your formal verification skills.
What is LeetLean?
LeetLean is a competitive programming platform focused on formal verification using the Lean 4 programming language. Instead of writing algorithms, you write mathematical proofs and verified programs.
How It Works
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 Lean 4 editor powered by lean4web. 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.
Problem Categories
Logic & Propositional
And, Or, Implies, Not, Iff
Natural Numbers
Induction, recursion, arithmetic
Algebraic Structures
Groups, rings, monoids
Program Verification
Verify correctness of algorithms