monogate.dev — eml math language workbench

Math you can check.
Compiled to C, Verilog and Lean.

EML is a single-operator math language — every expression reduces to one primitive, eml(x, y) = exp(x) − ln(y). A kernel's contract compiles to a Lean theorem, and Lean reports whether it is proved. The same source compiles to C, Python and Verilog with the compiler pip install monogate-forge gives you, and every compile command on this site is run against that release before each deploy.

CPythonVerilogLean
Start with Level 1 →Open Electronics LabLearn EML
MachLib theorems
7 600+
machine-checked in Lean 4 · machlib.org
Board captures
FPGA / Arty A7
16 capture packets · none for ESP32 / Arduino, Other · lab SOURCE.json, 2026-07-25
Status feed
monogate.net
renders machlib's CI status file
Start here
courses · esp32 / fpga / robotics
Electronics Lab
Hands-on hardware courses that start in a simulator, each with its evidence boundary stated. Board captures on record: FPGA / Arty A7.
tutorials · quick start
Learn EML
Step-by-step courses in EML and Forge: write a kernel, compile it, and read Lean's verdict on its contract.
what you can re-run
Reproduce
Install the compiler you get from PyPI, run the commands this site checks, and see which checks run on private repositories.
How it works

From a formula to generated code and a Lean verdict.

The loop: write the kernel, compile it, ask Lean what is proved, then measure it on a board if you have one wired up.

01
Write a kernel
A function with requires and ensures. Learn EML starts here.
02
Compile it
pip install monogate-forge, then eml-compile to C, Verilog, Lean and more.
03
Ask Lean what is proved
Run #print axioms against MachLib. No sorryAx in the list means the theorem is proved.
04
Take it to hardware
The Electronics Lab's courses start in a simulator. Board captures on record: FPGA / Arty A7; none for ESP32 / Arduino, Other.
05
Go deeper
The research record lives on monogate.org, and the Lean library the lessons' theorems import on machlib.org.
Surface split: monogate.dev is the workbench, monogate.org is the research record, machlib.org is the Lean library the lessons' theorems import, monogate.net renders machlib's CI status file, and 1op.io is games and visualization.