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

**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 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_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.

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

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