← Home/World 1
BMUCO Studio

World 1: The Meta-Proof Trap

In this world, you'll encounter proofs that look right but might not be. Your job is to fill in the formal Lean steps — and to decide whether the informal proof you're reading is actually valid. Not all of them are.

Requires: Natural Number Game
1
zero_add
2
succ_ne_zero
🔒
add_zero
Locked
🔒
add_succ
Locked
🔒
add_comm
Locked
🔒
mul_zero
Locked
🔒
add_assoc
Locked
🔒
add_eq_mul
Locked
Start World 1