MachLib
For machines, by machines.
import MachLib.EML — 4.77s build — 449 records
A machine-native formal mathematics library.
Fed by Forge. Trained on by agents. Verified by the Lean kernel. Zero Mathlib dependency.
What MachLib is, in four numbers.
A small, fast, fully-typed corpus that an agent can clone, build, and search end-to-end on a laptop. No Mathlib, no surprises.
The full chain — equation to proof.
MachLib is the verification layer of a complete toolchain. It works on its own, but it really shines when the whole stack is wired up. Here's the path a single equation takes.
You own every line from equation to silicon to proof.
No vendor. No external library. No 45-minute builds. No permission.
Why a separate library?
Mathlib is a monumental human achievement. It was not built for agents — it's slow to import, sparse on metadata, and silent about the proofs that didn't work. MachLib is the opposite of that, on purpose.
Mathlib import
- 45 minute cold build
- ≈500,000 lines of dependencies
- No chain-order annotations
- No difficulty lanes
- No tactic trace, no failure data
- No common-mistake corpus
- Built for human mathematicians
MachLib import
- 4.77 second cold build
- ~500 lines of foundations, axiomatic ℝ
- Chain-order annotations on every record
- 6 difficulty lanes (foundations → open problems)
- Tactic trace + success rate per tactic
- Common-mistake corpus per theorem
- Built for machines and the agents that train on them
Eight sections per theorem.
Every MachLib record is a self-contained training example. A single theorem ships with formal + informal statements, multiple proofs, tactic traces, common mistakes, structural profile, and relationships. One record, one JSON file, no ambient state.
{
"schema_version": "1.0.0",
"theorem": {
"id": "depth_of_const",
"statement": {
"informal": "The depth of a constant-leaf EML tree is zero. A bare constant has no `ceml` operations to count.",
"formal_lean": "theorem depth_of_const (c : ℂ) : (EMLTree.const c).depth = 0 := rfl"
},
"domain": "eml",
"lane": 1,
"tags": [
"depth",
"definition",
"rfl",
"lane-1"
]
},
"proofs": [
{
"id": "p1",
"tactics": [
"rfl"
],
"tactic_count": 1,
"eml_node_cost": 1,
"style": "definitional",
"is_optimal": true
}
],
"difficulty": {
"lane": 1,
"label": "beginner",
"prerequisite_skills": []
},
"common_mistakes": [
{
"why_fails": "Using `simp [EMLTree.depth]` works but is overkill — `rfl` already suffices."
},
{
"why_fails": "`by decide` fails because `EMLTree.depth` is not a `Decidable` proposition."
}
],
"structural_profile": {
"chain_order": null,
"drift_risk": "LOW",
"dynamics": {
"oscillations": 0,
"decays": 0
}
},
"relationships": {
"structural_siblings": [
"depth_ceml_pos",
"exp_in_EML_one"
]
},
"metadata": {
"verified": true,
"verification_method": "lean4_kernel"
}
}Six engines feed the corpus.
MachLib is not a snapshot. It's a pipeline. New records arrive from synthesis, compilation, RL training, search, contribution, and cross-domain bridging — each engine sealing its outputs into the same schema.
Synthetic Generation
Five strategies — constant_swap, domain_change, operator_swap, composition_depth, negation — fan a single base theorem into a family of structurally related variants. 414 of today's 449 records came from this engine.
Forge Mining
Every @verify(lean) annotation in Monogate Forge emits a Lean obligation. When Forge compiles an industrial vertical, MachLib gains the precision and overflow theorems that vertical demands.
Proof Gym (RL)
A Gymnasium-compatible Lean environment with a 54-tactic vocabulary. Agents discover non-obvious proofs; successful trajectories are added back into the corpus along with their tactic traces.
Multi-Proof BFS
For each theorem, breadth-first search enumerates alternative proofs shorter or different from the canonical one. MachLib stores all of them — is_optimal is a property, not a chosen branch.
Community
Lean developers contribute new theorems through pull requests. Every PR runs the schema validator + lake build + structural sibling check. Accepted records inherit the contributor's name in metadata.
Cross-Domain
When a structural sibling is discovered between two domains (Gaussian ↔ photoreceptor, sigmoid ↔ attention), the relationship is recorded on both endpoints. The corpus densifies as it grows.
For machines, by machines.
Mathlib is the canonical formal-mathematics library, and a monumental gift to the world. It was built — over fifteen years, by hundreds of contributors — for human mathematicians. Its proofs are dense, idiomatic, and chained through hundreds of files of inheritance.
An agent that needs to verify a single equation does not need that. It needs an axiomatic real number, four arithmetic operations, exp, log, sin, cos, and a small number of identities. That fits in ~500 lines.
MachLib is what you get when you put metadata first and history second. Every theorem ships with the things an agent actually consumes during training: chain order, difficulty lane, tactic trace, common mistakes, structural siblings. The proofs are there too, but they are no longer the only signal.
Academia has said, of agentic mathematics, that it does not belong in Mathlib. They may be right. So we made a different library — one that does belong to the agents.
Three ways in.
Pick the one that matches what you do today. The corpus, the foundations, and the contribution loop are all already live.
ML researchers
Pull the corpus from Hugging Face. 449 records, schema v1.0.0, one JSON file per theorem. Drop it into your training loop.
Agent builders
Use the Lean foundations as the verification target. Your agent writes a proof, lake build checks it in seconds, no Mathlib in the way.
Lean developers
Contribute. The schema is documented; the validator runs on every PR. Add a theorem, add its tactic trace, add the mistakes that don't work. The corpus grows from there.
Part of a larger stack.
MachLib is the foundations layer. The Forge compiles to it, CapCard certifies on top of it, PETAL verifies through it, 1op visualises what runs on it. Each piece is independently useful — together they form a verified, agent-native math toolchain.