MechMath

MechMath is an automated theorem-proving workflow for Lean 4. It turns informal mathematical reasoning into checked Lean proofs, uses Lean feedback to repair failed attempts, and decomposes hard proof states into smaller verified subgoals.

The accompanying paper refers to the workflow as Mechanic. This repository uses MechMath as the project name.

Overview

Large language models can often sketch plausible mathematical arguments, but full Lean formalization remains brittle. A single failed proof block can hide many independent subgoals, and repeatedly asking a model to fix the whole file usually gives it a growing, noisy context.

MechMath follows a sorry-driven decomposition strategy:

1. Generate or refine an informal solution.
2. Translate the solution into Lean and repair it with Lean feedback.
3. When direct repair fails, replace failing proof blocks with sorry to keep the verified proof skeleton.
4. Extract the remaining tactic states as clean subproblems.
5. Solve subproblems recursively and assemble the final proof.

This keeps successfully verified structure intact while giving the model smaller and more precise proof obligations.

Main Components

• Reasoner LLM worker: generates informal proof sketches and derives useful premises from Lean tactic states.
• Prover LLM worker: writes Lean proof attempts and revises them using Lean diagnostics.
• Prover worker: optional fast prover endpoint used when experiment.fast_prove.use_prover=true.
• Lean worker: calls the configured Lean server, captures diagnostics, and queries search backends.
• Sorrifier: localizes failures by replacing invalid proof blocks with sorry, then extracts unresolved subgoals.
• Proof manager: coordinates theorem-level solving, recursive subgoal solving, caching, and result recording.
• Observability: writes local logs/results and can optionally use W&B and Weave.

Repository Layout

.
├── assets/
│   ├── results/              # Completed Lean proofs from selected benchmarks
│   └── workflow.png          # Workflow diagram used in this README
├── configs/                  # Hydra configs for data, output, Lean, LLMs, logging
├── data/                     # JSONL datasets and Lean benchmark files
├── main.py                   # Hydra CLI entry point
├── scripts/                  # Convenience run scripts and utilities
├── src/mechmath/
│   ├── config.py             # Dataclass-backed config schema
│   ├── io/                   # Dataset loading and proof-frame persistence
│   ├── lean/                 # Lean client helpers, parsing, search, sorrification
│   ├── models/               # Proof-frame, Lean-code, and message models
│   ├── observability/        # Loguru, W&B/Weave, and run recorder integration
│   ├── prompt/               # Prompt templates for reasoning, proving, and repair
│   ├── proof_manager.py      # Recursive proof orchestration
│   ├── proof_runner.py       # Proof-frame execution helper
│   ├── utils.py              # Shared utilities
│   └── workers/              # LLM, prover, Lean, and reasoner workers
├── pyproject.toml
└── uv.lock

Installation

MechMath is managed with uv and requires Python 3.12 or newer.

uv sync

Lean-facing workflows also require a Lean 4 verification server. The bundled configs expect an HTTP Lean server at http://localhost:8088 by default. Update configs/lean/lean_server.yaml or pass a Hydra override if your server uses a different endpoint. For example, append this override to any run command:

lean.base_url=http://localhost:8088

Configuration

The default Hydra config is configs/config.yaml. It composes:

• configs/logging/ for Loguru plus optional W&B/Weave logging.
• configs/lean/lean_server.yaml for Lean integration.
• configs/llm/ for OpenAI-compatible LLM provider settings.
• configs/paths/ for input data and output roots.

Provider configs are public templates. Keep real credentials in environment variables or private Hydra overrides instead of committing secrets.

Common runtime fields:

• paths.data.root: directory containing JSONL or Lean input files.
• paths.data.problems: one file name or a list of file names under paths.data.root.
• paths.data.size: number of examples to load; -1 means all available examples.
• paths.data.offset: number of JSONL rows to skip before loading.
• paths.data.default_header: whether to prepend MechMath's default Lean header.
• experiment.batch_size: number of top-level problems to run concurrently.
• experiment.max_concurrency: concurrency inside one problem's proof tree.
• experiment.skip_existing: skip problems that already have a success, failed, or incomplete marker.
• experiment.fast_prove.use_prover: enable the optional prover endpoint.
• experiment.formal_prove_fix.use_llm_prover: use the configured proverllm for formal proof repair. This is the field read by main.py when selecting the formal prover LLM config.
• experiment.formal_prove_fix.search_n: number of Lean search results to use during repair.

Running

Show the Hydra CLI options:

uv run python main.py --help

Run the small JSONL example:

uv run python main.py --config-name=example_jsonl

Run the Lean-file example:

uv run python main.py --config-name=example_lean

Run miniF2F with the provided script:

bash scripts/run_minif2f_test.sh          # first 10 problems
bash scripts/run_minif2f_test.sh 50       # first 50 problems
bash scripts/run_minif2f_test.sh 50 10    # 50 problems after skipping 10 rows
FORCE=1 bash scripts/run_minif2f_test.sh  # rerun even when markers exist

Run ProverBench number theory:

bash scripts/run_proverbench_nt.sh

The provided benchmark scripts expect OPENROUTER_API_KEY, a W&B login or WANDB_API_KEY, and a reachable Lean server at http://localhost:8088.

Override model settings from the command line:

uv run python main.py \
  --config-name=example_jsonl \
  llm@reasonerllm=gpt-codex \
  llm@proverllm=gpt-codex \
  reasonerllm.api_key="$OPENAI_API_KEY" \
  proverllm.api_key="$OPENAI_API_KEY"

Data

MechMath accepts JSONL benchmark records and .lean files.

JSONL rows are converted into ProofFrame objects with these fields:

• formal_statement: Lean theorem or proof target.
• informal_prefix: optional informal statement or solution context.
• header: optional Lean imports/options. Used when paths.data.default_header=false.
• name: optional problem identifier.
• split: optional benchmark split metadata.

Lean files are loaded directly. When paths.data.default_header=true, MechMath uses its default Mathlib header; otherwise the file content is used as-is.

Bundled examples include:

• data/minif2f_test.jsonl
• data/proverbench_number_theory.jsonl
• data/Putnam2025/*.lean
• data/IMO2025/*.lean

Outputs

Runtime outputs are written under paths.output.root and grouped by project.name. With the default output config this is:

output/<project.name>/

For each problem, MechMath creates a problem directory containing cached proof state, intermediate records, and one terminal marker such as:

• <problem>_success.jsonl
• <problem>_failed.jsonl
• <problem>_incomplete.jsonl

Log files are written under logs/<project.name>/ by the default Loguru configuration. Hydra also uses that path as its run directory.

Formalized Results

The repository includes Lean proofs completed by MechMath for recent olympiad and competition benchmarks:

• IMO 2025 formal proofs
• Putnam 2025 formal proofs

These files record final formalized proofs produced by the workflow and can be inspected as standalone Lean artifacts.

Citation

@inproceedings{
  qiu2026mechmath,
  title={MechMath: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving},
  author={Ruichen Qiu and Yichuan Cao and Junqi Liu and Dakai Guo and Xiao-Shan Gao and Lihong Zhi and Ruyong Feng},
  booktitle={3rd AI for Math Workshop: Toward Self-Evolving Scientific Agents},
  year={2026},
  url={https://openreview.net/forum?id=a4idI3jLJn}
}