Rebuild lean-bench: pages in, verified indexed Lean out

Replaces the previous tree entirely. The pipeline is four separable pieces, each testable on its own: 1. leanbench/llm.py provider-neutral OpenAI-compatible connector, stdlib only, with retries, JSON coercion and a scripted client so the rest of the code is testable without a network. 2. leanbench/detect.py per-page detection of formalizable mathematics. Case 1 is mathematics asserted as fact (definition/theorem/lemma/..., deliberately not sub-classified); case 2 is a problem left open to the reader. Hits come back as spans -- start page and index, end page and index -- so several per page is normal. A hit cut off by the page end makes the detector re-read that page together with the next, repeatedly, so an item spread over three pages is found whole. Offsets come from verbatim quotes resolved by leanbench/anchors.py (exact -> whitespace-insensitive -> fuzzy), because models quote well and count badly. 3. leanbench/formalize.py + leanbench/verify.py each span becomes one Lean 4 declaration, judged by the real compiler: full elaboration for case 1, statement legality only for case 2, which has no proof to check. Lean's own diagnostics feed back for a repair attempt. "verified" (Lean accepted it) and "proved" (accepted with no sorry) are kept strictly apart. 4. leanbench/db.py indexed SQLite plus JSONL export. Every item is indexed by the types of its inputs, or by its own type when it is not a proof, and records the source book (sha256) and the page it starts on -- so `drop --source H --pages A-B` followed by a re-ingest redoes exactly those pages and nothing else. Infrastructure: - lean/ Lake project pinned to Mathlib. - docker/ image carrying Lean 4 and a prebuilt Mathlib. The Mathlib revision and the toolchain are resolved against each other at build time rather than both hardcoded, so the build does not rot. docker/smoke.py runs the whole pipeline inside the image against the real compiler, with the LLM scripted. - .gitea/workflows ci (lint + tests in a venv, since the runner image's Python is Debian-managed and refuses installs into itself), docker (build, verify, optionally push), ingest (submit a book by hand). The docker workflow is not a throwaway build: it leaves the image, the layer cache, an idle `lean-bench` container and the `lean-bench-data` / `lean-bench-books` volumes in place on the runner, and never prunes, so the environment is there to be used afterwards. Pushing to the registry is optional and cannot fail the build -- Gitea's container registry does not accept the built-in Actions token, so that needs a REGISTRY_TOKEN secret with write:package. 58 tests; they need neither network nor Lean. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Ci5T3gWDhhmqDec3e1XtYZ
2026-09-19 07:16:37 +00:00
commit b9e37952e6
38 changed files with 4548 additions and 0 deletions
@@ -0,0 +1,199 @@
+# 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 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.
+- **`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.