Zayden-Jung
d3555d9a52
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.
Also: 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), and .gitea/workflows for tests,
image build and push to the Gitea registry, and a manual "submit a book" run.
58 tests; they need neither network nor Lean.
168 lines
7.3 KiB
Markdown
168 lines
7.3 KiB
Markdown
# 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.
|
||
- **`docker`** — builds the Lean 4 + Mathlib image, proves Mathlib really elaborates
|
||
inside it, and pushes it to this Gitea's container registry. 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,
|
||
and the database plus JSONL export come back as artifacts.
|
||
|
||
Set the `DASHSCOPE_API_KEY` secret for `ingest`. The registry login uses the built-in
|
||
Actions token; add a `GITEA_TOKEN` secret with `package:write` if yours is restricted.
|
||
|
||
## 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.
|