Primary evidence
- LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem ProvingS1 · Primary research · Paper · 2025-06-27
- LeanConjecturer generation and evaluation repositoryS1 · Primary research · Repository
LeanConjecturer scales LLM-generated mathematical conjectures inside Lean
The pipeline extracts definitions and theorem context from Lean files, asks an LLM to propose new formal statements, checks generated statements through Lean and separates harder candidates for subsequent training.
What happened?
The LeanConjecturer paper reported generating 12,289 university-level Lean conjectures from 40 Mathlib seed files, of which 3,776 were syntactically valid and not discharged by the chosen `aesop` non-triviality filter, and showed that such generated problems could support domain-specific reinforcement learning for theorem proving.
The pipeline extracts definitions and theorem context from Lean files, asks an LLM to propose new formal statements, checks generated statements through Lean and separates harder candidates for subsequent training. The paper also reports several non-trivial topology examples as evidence that the pipeline can produce mathematically useful statements rather than only superficial perturbations.
Why it matters
Formal theorem provers depend heavily on available theorem statements and training tasks. LeanConjecturer supplied a reproducible route for expanding that problem distribution from the formal library itself and linked conjecture generation directly to reinforcement-learning data creation.
Significance rationale: LeanConjecturer made conjecture generation a scalable formal-mathematics pipeline rather than an occasional by-product of theorem proving, combining Mathlib context extraction, LLM generation and Lean-based filtering to create large numbers of candidate training problems.
Historical context
Earlier developments
Later developments
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- Autonomous primary role
- Formal assurance
- Artifact available
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Symbolic
- AI contribution
- Language models generate candidate Lean theorem statements from extracted mathematical context, while Lean and rule-based filters test syntax and selected notions of non-triviality before candidates are reused for training.
- Human contribution
- Researchers designed the context-extraction and filtering pipeline, chose seed files and evaluation criteria, conducted reinforcement-learning experiments, and analyzed representative generated statements.
- Verification
- Paper released · E3 · Inspectable artifact · Artifact available
- Last reviewed
- 2026-09-11
Technical details
- Systems
- leanconjecturer, lean, mathlib
- Organizations
- auto-res
- Problems
- formal-conjecture-generation, theorem-proving-data-scarcity
- Methods
- conjecture-generation, synthetic-formal-data, context-extraction, reinforcement-learning, lean
Sources & artifacts
- LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem ProvingS1 · Primary research · Paper · accessed 2026-09-11
- LeanConjecturer generation and evaluation repositoryS1 · Primary research · Repository · accessed 2026-09-11
- LeanConjecturer formal conjecture-generation pipelineArtifact · Code
Verification history
- 2025-06-27 · Paper released · E2 · Research record
The arXiv research record introduced LeanConjecturer and reported the generated-conjecture counts, filtering procedure and theorem-proving training results.
- 2026-09-11 · Paper released · E3 · Inspectable artifact
The public LeanConjecturer repository exposes the generation and evaluation pipeline. The generated data directory is not committed in the repository, so E3 records inspectable implementation rather than independent verification of the paper's novelty claims or every generated theorem.
Corrections
No corrections recorded.