lean-bench

Point it at a mathematics book. It finds the mathematics worth formalizing, turns each piece into Lean 4, asks the Lean compiler whether that Lean is legal, and files the result in a database indexed by the types each item is about.

book.pdf ──▶ detect ──▶ formalize ──▶ verify (Lean) ──▶ indexed database
              │             │             │                    │
        spans across   Lean 4 code   statements for       searchable by the
        pages, two     per item      open problems,       types an item takes
        kinds of hit                 proofs when given    in, or is

The four pieces

1. The LLM connector — leanbench/llm.py. Stdlib only, no SDK. Any OpenAI-compatible /chat/completions endpoint: DashScope/Qwen by default, equally happy with vLLM, Ollama, DeepSeek or OpenAI. Retries, JSON coercion, and a ScriptedClient so the rest of the code is testable without a network.

2. Detection — leanbench/detect.py. For every page, two questions:

• Case 1, statement — is there mathematics asserted as fact here? A definition, theorem, proposition, lemma, corollary, a precise claim inside an example. The kind is deliberately not recorded: all that matters is that it can become useful Lean 4.
• Case 2, problem — is there a question left open to the reader? An exercise, an unsolved problem. Formalizable too, as a statement with no proof.

Each hit is returned as a span:

{"kind": "statement", "label": "Theorem 1.6.3",
 "start_page": 41, "start_index": 1832,
 "end_page": 42,   "end_index": 96,
 "spans_pages": 2, "truncated": false}

Indices are character offsets into that page's text, so several hits per page are normal and each is addressable. If a passage runs off the bottom of the page, the model says so, the page is re-read together with the next one, and that repeats — so an item spread over three pages is found whole, not in fragments. The limit is --window (default 3); an item still cut off at the limit is stored with truncated: true rather than silently clipped.

Models cannot count characters, so they are never asked to. They quote the first and last few words verbatim, and leanbench/anchors.py turns those quotes into exact offsets — exact match, then whitespace-insensitive match (PDF line breaks), then fuzzy match. A quote that matches none of the three is reported as unresolved, never guessed at.

Reading the page, when the PDF lies

Many mathematics PDFs carry their formulas in fonts with custom encodings. They look right on screen and extract as nonsense. Two different failure modes, both present in this project's test book:

what the page says	what pymupdf extracts
Z_ab ≅ Z_a ⊕ Z_b, [x]_ab ↦ ([x]_a, [x]_b)	Zab Š Za ˚ Zb; defined by Œxab 7! .Œxa; Œxb/.
I + J = {a + b : a ∈ I and b ∈ J}	I C J D fa C b W a 2 I and b 2 J g

The second is the dangerous one: it is made of ordinary ASCII — D is =, C is +, 2 is ∈, W is : — so nothing looks wrong until you read it. No prompt recovers either, because the information is gone before the model sees the text.

--extractor ocr renders each page and reads the pixels with a vision model, over the same endpoint and key the rest of the pipeline uses. On the page above that turns the first row's garbage into $\mathbb{Z}_{ab} \cong \mathbb{Z}_a \oplus \mathbb{Z}_b$. Transcriptions are cached on disk by (document hash, page, dpi, backend), so a re-run costs nothing and an interrupted run resumes.

lean-bench extract book.pdf --pages 90 --compare   # see both, decide
lean-bench ingest book.pdf --pages 85-110 --extractor ocr

--extractor auto reads embedded text and OCRs only pages that fail a quality check, which is cheaper on books where the damage is patchy. The check scores both failure modes above; be aware it is a heuristic over character statistics, not a judgement about meaning. On a badly encoded book auto converges on ocr anyway — in the test book 89% of pages fail it — so if a spot check shows the maths is mangled, just use ocr and skip the guessing.

--ocr-backend tesseract is available offline. It is good at prose and poor at mathematics, which is the wrong way round for this job; treat it as a fallback.

3. Formalization and verification — leanbench/formalize.py, leanbench/verify.py. Every detected span becomes one self-contained Lean 4 declaration, which Lean then judges:

item	what is checked
statement with a proof in the book	the whole declaration, proof included
statement without one	the statement elaborates; the proof is sorry
problem (case 2)	statement legality only — there is no proof to check

When Lean rejects the code, its diagnostics go straight back to the model for one more attempt (LEANBENCH_REPAIR_ATTEMPTS). Two flags are kept apart on purpose: verified means Lean accepted it, proved means Lean accepted it with no sorry anywhere.

4. The database — leanbench/db.py. SQLite, indexed, plus a JSONL export for git. Each item records:

• its Lean code, imports, and what Lean said;
• the types it is indexed under — for a proof, the types of its inputs and hypotheses; for a definition, the type of the thing being defined. That is what makes one item relevant to another, and it is what search runs on;
• which book (sha256 of the file) and which page it starts on.

So any part of any source can be redone without touching anything else:

lean-bench drop --source <hash> --pages 30-45   # forget those pages
lean-bench ingest book.pdf --pages 30-45        # and do them again

Re-ingesting does this for you: a run over pages 30–45 deletes exactly the items filed under those pages first. Item identity is sha1(book hash + span), so the same passage of the same book is always the same row.

Quick start

pip install -e ".[dev]"
cp .env.example .env          # put your API key in it
lean-bench doctor             # is the LLM reachable? is Lean installed?

lean-bench ingest book.pdf --pages 30-60 --export datasets/items.jsonl
lean-bench stats
lean-bench search --type Int --role input --kind problem --code

Lean verification needs a Lean project with Mathlib built. Without one, everything still runs and nothing claims to be verified. With Docker you get one for free:

docker run --rm -e DASHSCOPE_API_KEY \
  -v "$PWD/books:/books" -v "$PWD/data:/data" \
  gitea.entroia.com/zayden-jung/lean-bench:latest \
  ingest /books/book.pdf --pages 30-60

Commands

lean-bench doctor	check the LLM, Lean and PDF wiring
lean-bench ingest SRC	the whole pipeline; --pages, --no-verify, --export
lean-bench extract SRC	show the page text that would be read; --compare puts both extractors side by side
lean-bench detect SRC	detection only — no Lean, no database
lean-bench search	by --type, --role, --kind, --page, --text
lean-bench sources / stats	what is in the database
lean-bench export OUT	JSONL dump
lean-bench drop --source H	forget a source, or --pages of it

Sources may be PDFs, or .txt files whose pages are separated by form feeds (what pdftotext emits).

Configuration

All environment, all optional, all overridable in .env:

variable	default
LEANBENCH_LLM_MODEL	qwen-max
LEANBENCH_LLM_BASE_URL	DashScope's OpenAI-compatible endpoint
LEANBENCH_LLM_API_KEY_ENV	DASHSCOPE_API_KEY
LEANBENCH_DATABASE	database/leanbench.sqlite
LEANBENCH_MAX_WINDOW_PAGES	3
LEANBENCH_REPAIR_ATTEMPTS	1
LEANBENCH_EXTRACTOR	text (text / auto / ocr)
LEANBENCH_OCR_MODEL	qwen-vl-max
LEANBENCH_OCR_DPI	200
LEANBENCH_OCR_THRESHOLD	0.75
LEANBENCH_OCR_CACHE	.leanbench-cache/ocr
LEANBENCH_LEAN_COMMAND	["lake","env","lean"]
LEANBENCH_LEAN_PROJECT	unset (a Lake project with Mathlib built)

CI/CD

Three Gitea Actions workflows, for the ubuntu-latest / ubuntu-24.04 / ubuntu-22.04 runner:

• ci — lint and the full test suite on every push. No network, no Lean: the LLM is scripted and the compiler is faked, so it is fast and deterministic. It installs into a venv, because the runner image's Python is Debian-managed and refuses installs into itself (PEP 668).

• docker — builds the Lean 4 + Mathlib image and checks it honestly: Mathlib really elaborates inside it, and a scripted end-to-end run (docker/smoke.py) proves the pipeline writes a verified item to the database with the real compiler attached. The Mathlib revision and the Lean toolchain are resolved against each other at build time (docker/resolve-mathlib.sh), because hardcoding both is how image builds break two months later.

  The Lean steps are one Docker layer each, and each long one is wrapped in timeout. That is not tidiness: the Mathlib cache fetch is gigabytes, so it earns a layer that a later failure never invalidates, and a stalled lake step fails with a diagnosable message instead of sitting silent for hours. The build also runs with --progress=plain, because BuildKit's default renderer collapses a long step into one rewritten line and a stall then looks exactly like progress. There is deliberately no lake build of our own library: verification runs lake env lean <scratch file>, which needs Mathlib's oleans and nothing else.

• ingest — run by hand: submit a book (repo path or URL), pick a page range. It runs inside the long-lived container and the results stay in the volume; the artifact is just a copy.

What the runner needs

RAM	4 GB minimum, 8 GB comfortable
disk	~25 GB free where Docker stores images, 40 GB comfortable
docker	the CLI plus the host socket (or a docker-in-docker runner)

Memory is the real constraint, and it is not negotiable: loading Mathlib's environment needs several GB, and the pipeline does exactly that for every item it verifies, not just once at build time. Below the threshold Lean does not fail cleanly — it thrashes, prints nothing, and eventually something kills it. The docker workflow therefore checks the host's memory before it starts and refuses with an explanation rather than discovering it forty minutes in. Override with skip_size_check if you know better than the check does.

Disk is checked the same way, and measured where images actually land (docker info --format '{{.DockerRootDir}}') rather than wherever the job happens to be running. The margin looks generous because export unpacks the image a second time beside the copy the build already wrote: a host with 18 GB free built every layer of this image and then died on the last Mathlib olean while exporting.

Note that on Docker's containerd image store, images live under /var/lib/containerd, which data-root in daemon.json does not move — that setting only relocates /var/lib/docker. Moving image storage to another disk means relocating both.

The build is not a throwaway

When the docker workflow finishes, the runner host still has everything it built:

what	name
image	lean-bench:latest, lean-bench:sha-<commit>
layer cache	kept — nothing ever runs docker system prune, so a rebuild reuses Mathlib instead of refetching it
idle container	lean-bench (--restart unless-stopped)
volumes	lean-bench-data (the database), lean-bench-books

So you can use it directly, with no rebuild and no docker run:

docker cp your-book.pdf lean-bench:/books/
docker exec -e DASHSCOPE_API_KEY=sk-... lean-bench \
  lean-bench ingest /books/your-book.pdf --pages 30-60
docker exec lean-bench lean-bench search --type Int --role input --code

A rebuild leaves a running container alone rather than interrupting whatever is in it; re-run the workflow with refresh_service=true to move it onto the new image.

Secrets

name	kind	why
DASHSCOPE_API_KEY	secret	the LLM, for ingest
REGISTRY_TOKEN	secret	a personal access token with write:package. The built-in Actions token is not accepted by Gitea's container registry, so without this the image is not pushed — it is still built and kept on the runner, and the build does not fail
REGISTRY_USER	variable	only if the pushing account is not the actor

Research plan

The paper plan for this project (ACL 2027 target, ARR deadline 4 Jan 2027) lives in docs/research-plan.md, with the work list in docs/TODO.md and the acceptance-bar analysis in docs/acl-2027-bar.md.

Experiments have IDs (P0, E0-E11); the registry, phases, gates and conventions are in docs/experiments/README.md. CI runner and environment notes: docs/infrastructure/runner-lean435.md.

Browse the 65-item semantic simplex schema review by opening that HTML file in a browser after cloning, or downloading it from Git. It shows role schemas and Lean signature expressions; textbook passages and full assistant judgment explanations remain private. The schema design and replay instructions explain how the page is generated and which annotations still need review.

What this does not claim

Lean says whether the code is legal, and — when there is a proof — whether it is correct. It cannot say the Lean faithfully renders what the book meant. A well-formed statement of the wrong theorem passes every check here. confidence, match_method and the stored source_text are kept so that judgement stays possible; spot-check before trusting a dataset.

Source books are not committed. .gitignore keeps PDFs and extracted text out of the repository. The tracked schema review contains semantic annotations and Lean signatures, while source-inclusive inputs remain in the ignored data directory.