monogate.dev / learn
Two tracks. Pick one.
Write math in EML, inspect its cost profile, and emit selected targets, or practice Lean 4 proof work with the PETAL curriculum. Progress saves locally — pick up where you left off.
6 lessons · 30 minutes · beginner
EML-lang in 30 Minutes
Write math. Inspect profiles. Emit selected targets. No prerequisites beyond algebra. Level 2+ available after.
1.Your First Equation5 min
2.Constants and Real Math5 min
3.PID Controller5 min
4.Formal Verification5 min
5.Hardware Target5 min
6.Your Own Project5 min
0 / 6 done
Start Learning →
6 lanes · 39 exercises · progressive
Lean 4 for EML
Prove your math is correct. 6 lanes from beginner to expert.
Lane 1:Foundations4 records
Lane 2:Lower Bounds8 records
Lane 3:Advanced Properties6 records
Lane 4:Expert Proofs5 records
Lane 5:Open Problems15 records
Lane 6:Cross-Domain1 record
0 / 39 done
Start Proving →