AutoformBench is a benchmark for evaluating the formalization of mathematical statements in Lean 4. This source-free release contains 341 audited problems, clean-room grading workspaces, a deterministic Harbor adapter, and task-level leaderboard data.
The benchmark uses Lean v4.32.2 and Mathlib commit
905b95818eb32af7874a58b427f50c1711a5e96c.
Paper here
Performance and cost efficiency on the full 341-task benchmark. Select either figure to open its vector PDF.
The official ranking uses the full frozen 341-task benchmark in the paper's source-present evaluation condition. The linked task-level CSVs cover all 341 tasks.
| Rank | Model | Solved | Results |
|---|---|---|---|
| 1 | GPT-6 Astra | 281 / 341 (82.4%) | CSV |
| 2 | Opus 5 | 211 / 341 (61.9%) | CSV |
| 3 | GPT-5.6 Sol | 201 / 341 (58.9%) | CSV |
| 4 | Fable 5 | 181 / 341 (53.1%) | CSV |
| 5 | DeepSeek V4.1 Flash | 180 / 341 (52.8%) | CSV |
| 6 | Gemini 3.7 Flash | 179 / 341 (52.5%) | CSV |
| 7 | Kimi K3 | 165 / 341 (48.4%) | CSV |
| 8 | Sonnet 5 | 152 / 341 (44.6%) | CSV |
| 9 | Opus 4.8 | 150 / 341 (44.0%) | CSV |
Pass rates should be compared together with each run's model, agent scaffold, source access, tool access, token budget, and stopping policy. The CSV files preserve the reported token, cost, turn, and code-size measurements for reproducible analysis; the source excerpts used in those evaluations are not redistributed here.
This repository contains all 341 audited AutoformBench tasks. Task IDs are
listed in MANIFEST.csv.
| Path | Contents |
|---|---|
workspaces/ |
341 canonical Lean grading workspaces |
MANIFEST.csv |
Problem IDs, source groups, and graded declarations |
SOURCES.csv |
Bibliographic metadata and source URLs |
leaderboard_data/ |
Task-level evaluation outcomes |
harbor/ |
Deterministic Harbor 0.22 adapter and verifier images |
This release contains no textbook excerpts, textbook PDFs, informal source
files, model traces, accepted submissions, gold proofs, or internal audit
records. Source material can be obtained independently through the references in
SOURCES.csv.
Each workspace contains a trusted challenge, a submission skeleton, and a
clean-room grader. Pick an ID from MANIFEST.csv, then:
cd workspaces/<problem_id>
lake exe cache get
# Replace the target `sorry` declarations in Submission.lean.
lake testAuxiliary Lean code may be added under Submission/. A passing submission must
match the challenge statement, use only permitted axioms, pass Comparator, and
survive independent-kernel replay.
Generate the Harbor task view and validate the release:
make harbor-tasks
make checkThe generated harbor/tasks/ directory is intentionally not tracked. See the
Harbor guide for image construction and runner commands.
Please cite AutoformBench using CITATION.cff. Bibliographic
details for the mathematical sources are retained in SOURCES.csv.
AutoformBench is released under the Creative Commons Attribution-NonCommercial
4.0 International license (CC BY-NC 4.0). It is intended for
evaluation and research, not for use as training data; see NOTICE.
Referenced and downloaded third-party projects remain subject to their own licenses; see
THIRD_PARTY_NOTICES.md.