BMUCO Studio
Worlds
Progress from spotting surface-level red flags to conducting full Mathlib-standard reviews. 7 worlds, 50+ levels, one mission.
1
World 1: The Meta-Proof Trap
Fill in Lean proof steps and decide if informal proofs are valid. Not all of them are.
8 levels
World 2: Tactic GauntletComing Soon
Master core Lean 4 tactics through increasingly challenging proof puzzles.
8 levels
World 3: The Specification GameComing Soon
Write formal specifications that match informal requirements — and catch the mismatches.
8 levels
World 4: Induction LabComing Soon
Prove properties by induction, from simple base cases to nested structural recursion.
8 levels
World 5: Library ArchaeologyComing Soon
Navigate Mathlib to find lemmas, understand naming conventions, and chain library results.
8 levels
World 6: Proof RefactoringComing Soon
Take working but messy proofs and refactor them to Mathlib contribution standards.
8 levels
World 7: The ContributionComing Soon
Combine everything to write a real Mathlib-quality proof from scratch.
6 levels