Bridging the gap between the Natural Number Game and Mathlib.
You finished the Natural Number Game. You know what induction is. But Mathlib-quality contributions require a completely different skill set: naming conventions, generality, library integration, proof architecture, and style compliance. BMUCO Studio trains exactly those skills.
The quality gap
Most proofs that compile are still far from library-ready. Mathlib PR reviewers evaluate five dimensions that most newcomers never learn: style compliance, correct generality, library integration, API completeness, and documentation.
BMUCO Studio turns proof review into a game. Each level presents a Lean 4 proof that compiles — but contains real issues that would get it rejected from Mathlib. Your job is to find them.
Learning by reviewing
Research shows that reviewing flawed proofs builds deeper understanding than writing proofs from scratch. When you identify why a proof is too long, uses the wrong predicate, or reinvents an existing lemma, you internalise the standards that make Mathlib contributions successful.
The game is structured into 7 worlds, each focusing on a different review skill — from spotting surface-level red flags to conducting full Mathlib-standard reviews.
The 5-layer review methodology
Every proof review exercise is decomposed into five structured layers. Each layer captures a distinct skill that Mathlib contributors need.
Inventory
Identify the mathematical objects, properties, hypotheses, and conclusion. Search Mathlib for existing relevant results.
Type Skeleton
Choose the right level of generality. Reason about type class constraints and universe levels.
Statement
Write the formal statement. Choose the correct Mathlib-style name. Justify naming decisions.
Proof
Write the proof in Lean 4. Verify compilation via AXLE. Record tactic choices and alternatives considered.
Culture Check
Check Mathlib coverage, style compliance, API completeness. Flag generality and documentation issues.
Ready to level up?
Every proof you review builds the skills you need to make your first Mathlib contribution. Start playing now.
Start Playing