lean-bench/README.md

# 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:

```json
{"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.

```bash
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:

```bash
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

```bash
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:

```bash
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`:

```bash
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`](docs/research-plan.md), with the work list in
[`docs/TODO.md`](docs/TODO.md) and the acceptance-bar analysis in
[`docs/acl-2027-bar.md`](docs/acl-2027-bar.md).

## 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; only code and the short Lean datasets belong in git.