MathAdv

Dataset and evaluation scripts for "MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize".

MathAdv is a benchmark for evaluating advanced mathematical reasoning in both natural language and Lean 4. The repository contains the released JSONL data, Lean verification utilities, task runners for API and local models, model-specific launch scripts, and result summarization tools.

Repository Layout

.
├── data_4_9/
│   ├── full_problems.jsonl
│   ├── prover_problems.jsonl
│   └── combined_prover_problems.jsonl
├── scripts/
│   ├── run_llms.py
│   ├── run_provers.py
│   ├── verify_lean4.py
│   ├── prepare_data.py
│   ├── summarize_results.py
│   ├── nl_qa_runs/
│   ├── nl_equivalence_runs/
│   ├── computational_pass5_runs/
│   ├── junk_theorem_runs/
│   │   ├── data/
│   │   ├── results/
│   │   ├── run_experiment.py
│   │   └── summarize_results.py
│   └── models/
│       ├── openai/
│       ├── gemini/
│       ├── deepseek_api/
│       ├── deepseek_local/
│       ├── goedel/
│       ├── internlm/
│       └── lot/
├── configs/
├── env.md
└── requirements.txt

The main public artifacts are:

• data_4_9/: benchmark data in JSONL format.
• scripts/run_llms.py: natural-language and API-model evaluation runner.
• scripts/run_provers.py: local formal-prover evaluation runner.
• scripts/verify_lean4.py: Lean 4 verifier based on lake exe repl.
• scripts/summarize_results.py: summary utility for prover-style results.jsonl files.
• scripts/junk_theorem_runs/: LLM junk-theorem experiment, Lean fixtures, and published results.
• scripts/models/: model-family wrappers and reproducibility commands.

Setup

Create a Python environment and install the dependencies needed for the tasks you want to run.

python -m venv .venv
source .venv/bin/activate
pip install --upgrade pip
pip install openai google-generativeai anthropic python-dotenv
pip install regex sympy latex2sympy2 antlr4-python3-runtime word2number

The junk-theorem study has a smaller dependency set that can be installed separately with pip install -r scripts/junk_theorem_runs/requirements.txt.

For formal Lean 4 verification, install Lean/Lake and provide a Mathlib workspace with lake exe repl available. The scripts use these environment variables when set:

export BENCH_ROOT=/path/to/MathAdv
export LAKE_PATH=/path/to/lake
export LEAN_WORKSPACE=/path/to/mathlib4

See env.md for separate environment recommendations for local prover stacks such as DeepSeek-Prover, InternLM, Llemma, LeanOfThought, and LeanDojo.

Running Evaluations

Run commands from the repository root unless otherwise noted.

Natural-Language Tasks

scripts/run_llms.py evaluates multiple-choice, computational, transformed computational, and Lean 4 completion tasks for API or local Hugging Face models.

Multiple-choice:

python scripts/run_llms.py \
  --provider openai \
  --model gpt-4o \
  --task mc \
  --limit 5

Computational pass@5:

python scripts/run_llms.py \
  --provider openai \
  --model gpt-4o \
  --task computational \
  --computational-pass-k 5 \
  --limit 5

Natural-language suite without Lean verification:

python scripts/run_llms.py \
  --provider openai \
  --model gpt-4o \
  --task nl_suite

Supported providers include openai, deepseek, gemini, claude, llemma, and huggingface. API keys can be exported in the shell or placed in a local .env file, for example OPENAI_API_KEY, GOOGLE_API_KEY or GEMINI_API_KEY, ANTHROPIC_API_KEY, and DEEPSEEK_API_KEY.

Lean 4 Completion With API Models

For API models, run_llms.py --task lean4 asks the model to replace the final sorry and verifies the completed theorem.

python scripts/run_llms.py \
  --provider openai \
  --model gpt-4o \
  --task lean4 \
  --lean4-pass-k 32 \
  --lean4-resume \
  --lake-path "$LAKE_PATH" \
  --lean-workspace "$LEAN_WORKSPACE" \
  --limit 5

Junk-Theorem Study

scripts/junk_theorem_runs/run_experiment.py adds a diagnostic study for MathAdv, evaluating whether models can recognize and explain 15 Lean 4 junk theorems: formally valid statements whose surface readings are misleading. Each model receives the compile and meaning questions in separate, stateless conversations. The Lean units and grading manifest are in scripts/junk_theorem_runs/data/; model and prompt definitions are in models.json and prompts.json.

Copy the environment template and add the required API keys before making model calls:

cp scripts/junk_theorem_runs/.env.example scripts/junk_theorem_runs/.env
python scripts/junk_theorem_runs/run_experiment.py --smoke-test
python scripts/junk_theorem_runs/run_experiment.py --dry-run
python scripts/junk_theorem_runs/run_experiment.py
python scripts/junk_theorem_runs/summarize_results.py

The runner is resumable and supports --samples, --models, --theorems, --questions, and --workers filters. See scripts/junk_theorem_runs/README.md for the study design and reported findings.

Local Prover Models

scripts/run_provers.py reads data_4_9/prover_problems.jsonl, runs a local prover model, extracts Lean code, verifies it, and writes prover-style results.

Example smoke run:

python scripts/run_provers.py \
  --model deepseek_prover_v1_5 \
  --lake-path "$LAKE_PATH" \
  --lean-workspace "$LEAN_WORKSPACE" \
  --limit 5

Supported local prover choices are:

• deepseek_prover_v1_5
• deepseek_prover_v2
• internlm_math
• internlm2_step_prover
• llemma
• lean_of_thought

Model-specific wrappers and paper-style launch commands are available in:

• scripts/models/openai/GPT_RUN_COMMANDS.md
• scripts/models/deepseek_api/DEEPSEEK_RUN_COMMANDS.md
• scripts/models/gemini/GEMINI_RUN_COMMANDS.md
• scripts/models/deepseek_local/
• scripts/models/goedel/
• scripts/models/internlm/
• scripts/models/lot/

Category Filtering

Both main runners support category filtering:

python scripts/run_llms.py --provider openai --task mc --category abstract_algebra_4_9
python scripts/run_provers.py --model deepseek_prover_v1_5 --category abstract_algebra_4_9

Multiple categories can be passed by repeating --category or using comma-separated values.

Results

By default, the main benchmark runners write outputs under results/.

For run_llms.py, results are organized as:

results/llm/<provider>_<model>/
├── mc_results.jsonl
├── computational_results.jsonl
├── computational_transformed_results.jsonl
├── lean4_results.jsonl
└── raw_outputs/

For run_provers.py, results are organized as:

results/<model_name>/
├── results.jsonl
├── prompts/
├── raw_outputs/
└── extracted_for_verification/

The checked-in junk-theorem run is stored with its workflow:

scripts/junk_theorem_runs/results/
├── raw/
├── transcripts/
├── all_results.csv
├── meaning_grades.csv
└── summary.md

This published run contains 360 successful responses from four OpenAI and DeepSeek models. summary.md reports compile-verdict accuracy, meaning_grades.csv contains the manual 0–2 comprehension grades, and transcripts/ preserves the responses used for grading.

Summarize prover-style results with:

python scripts/summarize_results.py results/<model_name>/results.jsonl
python scripts/summarize_results.py results/<model_name>/results.jsonl --json

complete means the Lean verifier found no errors and no remaining sorry. pass means the Lean code produced no errors; for theorem proving scores, use complete unless reproducing an analysis that explicitly uses a different criterion.

Citation

If you use this benchmark, please cite the paper:

MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize

The BibTeX entry will be updated here when the final paper metadata is available.