A Practical Framework for Auto-Generating Missing Mathlib Libraries
LeanGenerator is an automated formal mathematical library generation system for Lean 4 and mathlib. It leverages LLMs and a self-synthesizing code harness to automate the full pipeline—definition → lemma → theorem → proof → compilation → packaging—for domains not yet covered in mathlib.
Inspired by AutoHarness, the core innovation is treating the proof generation logic as learnable harness code that iteratively refines itself through Lean compiler feedback, rather than relying on static prompting or manual engineering. The output is a directly importable, verifiable, mathlib-compliant formal library.
Lean is intentionally designed for automated reasoning, proof search, and code synthesis.
by tidy: Automated proof simplification and cleanupby simp: Powerful term rewriting and simplificationaesop: Automated proof search with extensible tacticshint: Suggests relevant proof tactics
- Official Lean 4 models and LeanCopilot for real-time code completion
- Modern LLMs (GPT-4o, DeepSeek, etc.) generate syntactically correct Lean code
- Formal feedback loops enable self-correction
- Strong static typing and compiler-enforced correctness
- Proof search, repair, and validation are fully automatable
- Lean compiler error messages drive iterative harness refinement
Specify a target mathematical domain missing from mathlib.
Example: Tate pairing on elliptic curves over finite fields
- Retrieve papers, textbooks, and formal definitions
- Extract axioms, definitions, theorems, and properties
structure TatePairing (F : Type) [Field F] (E : EllipticCurve F) where
pairing : E → E → F
bilinear : ∀ P Q R, pairing (P + Q) R = pairing P R * pairing Q R
non_degenerate : ∀ P, (∀ Q, pairing P Q = 1) → P = 0lemma TatePairing.symmetric {F E} [Field F] [EllipticCurve E]
(t : TatePairing F E) :
∀ P Q, t.pairing P Q = t.pairing Q P :=
by sorryThis is the core engine of LeanGenerator, directly adapted from the AutoHarness methodology.
Three harness types mediate between the LLM and the Lean compiler:
| Variant | Description |
|---|---|
| Proof-Filter | Generates a set of candidate tactic sequences; LLM ranks by plausibility |
| Proof-Verifier | LLM proposes a proof; harness validates via compiler, rejects with error context |
| Tactic-Policy | Pure Python/Lean script selects tactics without runtime LLM calls (lowest cost) |
Core harness function signatures:
def propose_proof(goal: str) -> str:
"""Generate a candidate tactic sequence for the given proof goal."""
def is_valid_proof(goal: str, proof: str) -> bool:
"""Validate proof by invoking the Lean compiler; return True if no errors."""Initialize tree of harness code hypotheses
↓
Thompson Sampling → select node to refine
↓
Execute harness across 10 parallel Lean environments (up to 1000 steps)
↓
Collect up to 5 failed proof attempts with compiler error messages
↓
Feed errors + original harness code → LLM for mutation/refinement
↓
Update tree; repeat until compilation success rate = 100% or timeout
Termination criterion: compilation success rate reaches 100% across sampled theorems, or iteration budget exhausted.
Convergence: empirically, most proof domains converge within ~15 refinement iterations.
- Real-time type and syntax checking via Lean compiler
- Harness automatically repairs imports, type errors, and proof failures
- Iterative refinement until error-free; compiler errors are first-class feedback signals
- Auto-generate project directory structure
- Create
lakefile.toml - Manage import chains, documentation, and test files
- Ensure mathlib-compliant style and naming conventions
A buildable, importable Lean package ready for use or PR into mathlib.
| Category | Tools |
|---|---|
| Automated proving | aesop, simp, tidy |
| Code completion | LeanCopilot |
| Paper formalization | Formalize24, Lean Search |
| Harness execution | Parallel Lean 4 environments |
| Project scaffolding | Lake, lakefile.toml generator |
| Environment | Lean 4, mathlib, Lake |
- End-to-end generation of complete Lean libraries for missing domains
- Automatic creation of structures, typeclasses, definitions, lemmas, theorems
- Automated proof of low-to-medium difficulty theorems via harness refinement
- Full compilation, self-repair, documentation, and packaging
- Strict adherence to mathlib style and standards
- Smaller LLMs outperforming larger ones via learned harness (cost efficiency)
- Original mathematical research or open problem solving
- Fully unsupervised understanding of ambiguous natural language
- Fully automated proofs of deep mathematical theorems
- Harness as learnable code: The proof generation logic itself is refined through compiler feedback—not just the proofs
- Gradient-free optimization: LLM acts as a mutation operator; no fine-tuning required
- Paradigm shift: From single-theorem automation to library-level formal proof engineering
- Fill mathlib gaps: Rapidly generate folklore lemmas, niche branches, and connecting tissue
- Low cost: Small LLMs + learned harness can outperform large models; drastically faster than manual development
- Verifiable & reusable: Output is compile-ready, provable, and integrable
- Formal mathematics research: Rapidly prototype missing foundational libraries
- Education & tooling: Generate domain-specific mathematical modules
- AI + formal methods: Validate automated formalization pipelines
- Mathlib community: Batch-fill gaps in underrepresented domains