PETAL · Proof · Explanation · Tactic · Aligned · Lean
Learn Lean by Proving EML
39 hand-audited Lean 4 theorems from the Monogate formalization, structured as a 6-lane interactive curriculum. Every proof step has a natural-language explanation, the rationale for the tactic chosen, and common mistakes a beginner typically makes.
Dataset seed_v1 · schema 1.0.0 · monogate-lean source ↗ · CC BY 4.0
The 6 lanes
Lane 1First Contact4 records
Your first Lean proofs. Definitions. rfl.
Inductive types, depth, rfl, and the complex-exp identity. The smallest possible Lean proofs.
Start →
🔒 Lane 2Building Blocks8 records
Composition, simp, hypothesis-driven rewrites.
How simp, rewrites, and hypothesis-driven tactics chain definitions into composite results.
Complete Lane 1 to unlock Building Blocks
🔒 Lane 3Arithmetic from Nothing6 records
Witness extraction. F-family lower bounds. Proof-by-contradiction.
Witness extraction, F-family lower bounds, and proof-by-contradiction over EML trees.
Walk-through coming soon — view records on GitHub ↗
🔒 Lane 4The Other Operators5 records
SuperBEST framework. Multi-operator lower bounds. Synthesis lemmas.
The SuperBEST framework: multi-operator lower bounds and the synthesis lemmas they unlock.
Walk-through coming soon — view records on GitHub ↗
🔒 Lane 5Into the Complex Plane15 records
Universality. EML-elementary. Self-map conjugacies. Mathlib wrappers.
Universality, EML-elementary, self-map conjugacies, and how Mathlib wrappers connect to the master result.
Walk-through coming soon — view records on GitHub ↗
🔒 Lane 6The Barrier1 record
The research frontier. Open problems. Contribute here.
The research frontier — the InfiniteZerosBarrier and the open lemmas that gate sin/cos/π/i.
Walk-through coming soon — view records on GitHub ↗