Can you spot what's wrong with this proof in Lean?

Proofs that compile aren't always correct. Sharpen your proof review skills and level up from the Natural Number Game to Mathlib-ready contributions.

World 1

Smell Test

Completed the Natural Number Game? Great. Now spot surface-level red flags in Lean 4 proofs.

Level 1

The Bloated Proof

The Theorem

If n is a natural number, then n + 0 = n.

Lean 4 Code

1theorem add_zero_eq (n : ℕ) : n + 0 = n := by
2  induction n with
3  | zero =>
4    -- Base case: 0 + 0 = 0
5    simp [Nat.add_zero]
6  | succ k ih =>
7    -- Inductive step: (k + 1) + 0 = k + 1
8    rw [Nat.succ_add]
9    rw [Nat.add_zero]
10    rw [Nat.add_zero] at ih
11    have h1 : k + 0 = k := ih
12    have h2 : k + 1 = Nat.succ k := rfl
13    rw [← h2]
14    simp [Nat.add_zero]
15    -- Clean up remaining goals
16    rfl

Read the proof above carefully. When you're ready, start the review to see the checklist.

7 worlds. 50+ levels. One mission.

Progress from spotting surface-level red flags to conducting full Mathlib-standard reviews. Bridge the gap between the Natural Number Game and real library contributions.

Explore All Worlds →