MathRA

Part I. LeanGenerator: An automated Lean4 mathematical theorem proving synthesis tool.

System Architecture

LeanGenerator/
├── src/
│   ├── main.rs                  # CLI entry (synthesize / scan / check)
│   ├── lib.rs                   # Library module declarations
│   │
│   ├── core/                    # Core data types
│   │   ├── proof.rs             # ProofGoal, ProofAttempt, ProvedTheorem
│   │   ├── harness.rs           # HarnessNode, HarnessType (three Harness variants)
│   │   ├── state.rs             # ProofState, SynthesisState (synthesis session state)
│   │   ├── template.rs          # Template loading and rendering
│   │   └── error.rs             # HarnessError, Result types
│   │
│   ├── engine/                  # Synthesis engine
│   │   ├── synthesis.rs         # Main loop: Thompson sampling → generate → verify → update
│   │   ├── search.rs            # SearchTree: Harness node search tree
│   │   └── thompson.rs          # Thompson sampling (Beta distribution)
│   │
│   ├── sandbox/                 # Lean compiler sandbox
│   │   ├── executor.rs          # LeanExecutor: runs lean / lake build
│   │   └── config.rs            # SandboxConfig
│   │
│   ├── feedback/                # Feedback collection
│   │   ├── collector.rs         # FeedbackCollector: aggregates compilation results
│   │   └── types.rs             # FeedbackEvent, NodeFeedback
│   │
│   ├── lean/                    # Lean project integration
│   │   ├── project.rs           # LeanProject: scans sorries, writes back proofs
│   │   └── parser.rs            # LeanErrorParser: parses compiler error output
│   │
│   ├── llm/                     # LLM client
│   │   ├── client.rs            # LlmClient: supports Anthropic / OpenAI / DeepSeek
│   │   └── prompt.rs            # PromptBuilder: template rendering + global principle injection
│   │
│   └── templates/               # Harness implementations
│       ├── verifier.rs          # ProofVerifier: LLM proposes single proof, compiler verifies
│       ├── filter.rs            # ProofFilter: generates N candidates, takes first successful
│       ├── policy.rs            # TacticPolicy: deterministic policy, no LLM calls
│       └── refiner.rs           # ProofRefiner: repairs failed proofs from compilation errors
│
├── memory/                      # Prompt templates (customizable)
│   ├── global_principles.md     # Global proof principles (injected into all prompts)
│   └── templates/
│       ├── verifier.md          # ProofVerifier prompt template
│       ├── filter.md            # ProofFilter prompt template
│       ├── policy.md            # TacticPolicy prompt template
│       └── refiner.md           # Proof repair prompt template
│
├── examples/
│   └── analyticgeo.rs           # Example: run synthesis on an AnalyticGeometry project
│
├── Cargo.toml                   # Dependencies
└── leangenerator.toml           # Runtime configuration

---

How It Works

Lean project
    │
    ▼
[Scan sorry targets]  ←── LeanProject::scan_sorries()
    │
    ▼
[Thompson sampling selects Harness node]  ←── SearchTree + Beta distribution
    │
    ├── ProofVerifier  → LLM generates single proof
    ├── ProofFilter    → LLM generates multiple candidates, first valid wins
    └── TacticPolicy   → deterministic rule matching (ring / linarith / simp...)
    │
    ▼
[Lean compiler verification]  ←── LeanExecutor::validate()
    │
    ├── Success → record ProvedTheorem, update Beta(α+1, β)
    └── Failure → collect errors, update Beta(α, β+1)
              Every 5 rounds → spawn refinement child nodes (ProofRefiner)
    │
    ▼
[Write back to source files]  ←── LeanProject::patch_all()

Three Harness Types:

Type	Strategy	Use Case
ProofVerifier	LLM proposes one proof; compiler verifies	Equivalence propositions, existential proofs
ProofFilter	LLM generates N candidates, returns first valid	Existential discriminants, deep inequalities
TacticPolicy	No LLM; deterministic selection based on goal pattern	Algebraic identities, linear arithmetic

---

Requirements

• Rust 1.75+ (including Cargo)
• Lean 4 + Lake (required for target projects)
• LLM API Key (one of: Anthropic / OpenAI / DeepSeek)

---

Installation

# Clone repository
git clone <repo-url>
cd LeanGenerator

# Build in release mode
cargo build --release

# Executable location
./target/release/leangenerator

---

Configuration

1. Set API Key

# Anthropic (default)
export ANTHROPIC_API_KEY=sk-ant-...

# OpenAI
export OPENAI_API_KEY=sk-...

# DeepSeek
export DEEPSEEK_API_KEY=sk-...

2. Edit leangenerator.toml (optional)

[synthesis]
max_iterations = 50        # Maximum synthesis iterations
parallel_envs = 4          # Parallel goals per round
max_errors_per_feedback = 5
convergence_threshold = 1.0  # 1.0 = stop only when 100% of goals are proved

[sandbox]
lean_executable = "lean"
lake_executable = "lake"
timeout_secs = 60          # Single compilation timeout (seconds)
max_memory_mb = 2048

[llm]
provider = "anthropic"
model = "claude-sonnet-4-5"
max_tokens = 4096
temperature = 0.7
api_key_env = "ANTHROPIC_API_KEY"

[lean]
toolchain = "leanprover/lean4:v4.14.0"
mathlib_path = ".lake/packages/mathlib"

---

Usage

Scan sorry Targets

leangenerator scan --project /path/to/lean/project

Sample output:

Found 12 sorry goals:
  AnalyticGeometry/Ellipse.lean:42 — Ellipse.fromEllipse_onCurve
  AnalyticGeometry/Circle.lean:87 — Circle.dist_eq_radius
  ...

Run Proof Synthesis

leangenerator synthesize \
  --project /path/to/lean/project \
  --memory ./memory \
  --max-iterations 50 \
  --provider anthropic \
  --model claude-sonnet-4-5

Common arguments:

Argument	Default	Description
--project	.	Lean project root directory
--memory	memory	Prompt template directory
--max-iterations / -n	50	Maximum iterations
--provider	anthropic	LLM provider
--model	claude-sonnet-4-5	Model name
--timeout	60	Compilation timeout (seconds)
--patch	true	Whether to write back to source files

Check Project Compilation Status

leangenerator check --project /path/to/lean/project

---

Custom Prompt Templates

Edit .md files under memory/templates/ to adjust LLM proof strategies.

Template variables:

Variable	Description
{theorem_statement}	Theorem statement (including sorry)
{imports}	File import list
{context}	Namespaces, open statements, and surrounding context
{compiler_error}	Previous compilation error message
{num_candidates}	Number of candidates in Filter mode

---

Testing

# Run all unit tests
cargo test

# Run Thompson sampling tests
cargo test thompson

# Run Lean error parser tests
cargo test parser

---

Troubleshooting

Q: ANTHROPIC_API_KEY not set

export ANTHROPIC_API_KEY=your_key_here

Q: lean: command not found Ensure Lean4 is installed and in your PATH, or specify full paths in leangenerator.toml:

[sandbox]
lean_executable = "/home/user/.elan/bin/lean"
lake_executable = "/home/user/.elan/bin/lake"

Q: Synthesis timeouts Increase timeout_secs or reduce max_iterations:

[sandbox]
timeout_secs = 120

Q: Proof succeeded but writeback failed Check file write permissions, or manually paste the generated proof into the source file.