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.
                   One Docker layer per Lean step, each long one under `timeout`:
                   the gigabyte cache fetch earns a layer that a later failure never
                   invalidates, and a stalled step fails with a message instead of
                   sitting silent for an hour. There is deliberately no `lake build`
                   of our own library -- verification runs `lake env lean` against
                   Mathlib's oleans and needs nothing else, and building the library
                   was pure cost. 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 build 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.

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

tests/conftest.py

@@ -0,0 +1,79 @@
+from __future__ import annotations
+
+import json
+from pathlib import Path
+
+import pytest
+
+from leanbench.document import Document
+from leanbench.verify import MODE_FULL, VerifyResult
+
+PAGE_ONE = """Chapter 1. Divisibility
+
+1.6 Divisibility in the Integers
+
+Definition 1.6.1. Let a and b be integers. We say a divides b, written a | b,
+if there exists an integer k such that b = a k.
+
+Theorem 1.6.2. Let a, b and c be integers. If a divides b and a divides c,
+then a divides b + c.
+
+Proof. Write b = a k and c = a m. Then b + c = a (k + m). QED
+
+Theorem 1.6.3. Let a and b be nonzero integers. Then the set of common
+"""
+
+PAGE_TWO = """divisors of a and b has a greatest element, the greatest common divisor.
+
+Exercise 1.6.4. Show that if a divides b and b divides a, then a = b or a = -b.
+
+Exercise 1.6.5. Prove that the sum of two odd integers is even.
+"""
+
+
+@pytest.fixture()
+def two_page_book(tmp_path: Path) -> Document:
+    path = tmp_path / "book.txt"
+    path.write_text(PAGE_ONE + "\f" + PAGE_TWO, encoding="utf-8")
+    return Document.load(path, title="Test Book")
+
+
+class FakeChecker:
+    """A Lean stand-in: fails anything containing ``BAD``, otherwise accepts."""
+
+    def __init__(self) -> None:
+        self.calls: list[str] = []
+
+    def available(self) -> bool:
+        return True
+
+    def check(self, code: str, *, mode: str = MODE_FULL, imports=None) -> VerifyResult:
+        self.calls.append(code)
+        if "BAD" in code:
+            return VerifyResult(False, mode, False, "LeanBenchCheck.lean:3:0: error: bad")
+        return VerifyResult(True, mode, "sorry" in code, "")
+
+
+@pytest.fixture()
+def fake_checker() -> FakeChecker:
+    return FakeChecker()
+
+
+def detection_reply(items: list[dict]) -> str:
+    return json.dumps({"items": items})
+
+
+def formalize_reply(**overrides) -> str:
+    payload = {
+        "skip": False,
+        "reason": "",
+        "imports": ["Mathlib"],
+        "name": "test_decl",
+        "lean_code": "theorem test_decl (a b : Int) (h : a ∣ b) : a ∣ b := by\n  sorry",
+        "has_proof": False,
+        "informal": "a divides b",
+        "index_types": ["Int"],
+        "confidence": 0.8,
+    }
+    payload.update(overrides)
+    return json.dumps(payload)

tests/test_anchors.py

@@ -0,0 +1,54 @@
+from __future__ import annotations
+
+from leanbench.anchors import find, resolve_span
+
+TEXT = (
+    "Theorem 1.6.2. Let a, b and c be integers. If a divides b and a divides c,\n"
+    "then a divides b + c.\n\nProof. Write b = a k."
+)
+
+
+def test_exact_match() -> None:
+    match = find(TEXT, "Theorem 1.6.2.")
+    assert match is not None and match.method == "exact"
+    assert TEXT[match.start : match.end] == "Theorem 1.6.2."
+
+
+def test_whitespace_insensitive_match_across_a_line_break() -> None:
+    match = find(TEXT, "a divides c, then a divides b + c.")
+    assert match is not None
+    assert match.method == "whitespace"
+    assert TEXT[match.start : match.end].replace("\n", " ") == "a divides c, then a divides b + c."
+
+
+def test_fuzzy_match_survives_a_typo() -> None:
+    match = find(TEXT, "Let a, b and c be integres. If a divides b")
+    assert match is not None
+    assert match.method == "fuzzy"
+    assert "integers" in TEXT[match.start : match.end]
+
+
+def test_missing_anchor_is_reported_not_guessed() -> None:
+    assert find(TEXT, "nothing like this appears anywhere in the page") is None
+
+
+def test_resolve_span_covers_start_to_end() -> None:
+    span = resolve_span(TEXT, "Theorem 1.6.2.", "a divides b + c.")
+    assert span is not None and span.resolved
+    assert TEXT[span.start : span.end].startswith("Theorem 1.6.2.")
+    assert TEXT[span.start : span.end].endswith("a divides b + c.")
+
+
+def test_resolve_span_falls_back_when_the_end_quote_is_wrong() -> None:
+    span = resolve_span(TEXT, "Theorem 1.6.2.", "this ending was invented", fallback_length=40)
+    assert span is not None
+    assert "truncated" in span.method
+    assert span.end - span.start == 40
+
+
+def test_resolve_span_searches_forward_from_the_cursor() -> None:
+    text = "alpha beta alpha gamma"
+    first = resolve_span(text, "alpha", "beta")
+    assert first is not None and first.start == 0
+    second = resolve_span(text, "alpha", "gamma", search_from=first.end)
+    assert second is not None and second.start == text.rindex("alpha")

tests/test_db.py

@@ -0,0 +1,133 @@
+from __future__ import annotations
+
+import json
+from pathlib import Path
+
+import pytest
+
+from leanbench.db import Database, ItemRow, item_id
+
+
+def row(**overrides) -> ItemRow:
+    data = dict(
+        id="",
+        source_hash="book-hash-a",
+        kind="statement",
+        label="Theorem 1.6.2",
+        summary="divisibility is additive",
+        informal="a | b and a | c implies a | b + c",
+        start_page=12,
+        start_index=100,
+        end_page=12,
+        end_index=260,
+        page_checksum="abc",
+        source_text="Theorem 1.6.2 ...",
+        lean_name="dvd_add'",
+        lean_code="theorem dvd_add' (a b c : Int) : True := trivial",
+        imports=["Mathlib"],
+        has_proof=True,
+        verified=True,
+        proved=True,
+        verify_mode="full",
+        diagnostics="",
+        confidence=0.9,
+        match_method="exact",
+        match_score=1.0,
+        truncated=False,
+        types=[("Int", "input")],
+    )
+    data.update(overrides)
+    if not data["id"]:
+        data["id"] = item_id(data["source_hash"], data["start_page"], data["start_index"],
+                             data["end_page"], data["end_index"])
+    return ItemRow(**data)
+
+
+@pytest.fixture()
+def database(tmp_path: Path) -> Database:
+    db = Database(tmp_path / "test.sqlite")
+    db.upsert_source("book-hash-a", title="Algebra", path="a.pdf", pages=400)
+    yield db
+    db.close()
+
+
+def test_item_id_is_stable_for_the_same_span() -> None:
+    first = item_id("h", 1, 2, 3, 4)
+    assert first == item_id("h", 1, 2, 3, 4)
+    assert first != item_id("h", 1, 2, 3, 5)
+
+
+def test_store_and_read_back(database: Database) -> None:
+    identifier = database.upsert_item(row())
+    stored = database.get(identifier)
+    assert stored is not None
+    assert stored["imports"] == ["Mathlib"]
+    assert stored["types"] == [{"name": "Int", "role": "input"}]
+
+
+def test_reingesting_the_same_span_updates_rather_than_duplicates(database: Database) -> None:
+    database.upsert_item(row())
+    database.upsert_item(row(lean_name="renamed", types=[("Nat", "input")]))
+    assert database.stats()["items"] == 1
+    stored = database.get(item_id("book-hash-a", 12, 100, 12, 260))
+    assert stored is not None and stored["lean_name"] == "renamed"
+    assert stored["types"] == [{"name": "Nat", "role": "input"}], "stale types are dropped"
+
+
+def test_search_by_type_is_the_point(database: Database) -> None:
+    database.upsert_item(row(types=[("Int", "input")]))
+    database.upsert_item(row(start_index=500, end_index=700, kind="problem",
+                             types=[("Polynomial", "input"), ("Int", "input")]))
+    assert len(database.search(types=["Int"])) == 2
+    assert len(database.search(types=["Polynomial"])) == 1
+    assert len(database.search(types=["Int", "Polynomial"], match_all_types=True)) == 1
+    assert len(database.search(types=["Int"], kind="problem")) == 1
+
+
+def test_search_by_role_separates_definitions_from_theorems(database: Database) -> None:
+    database.upsert_item(row(types=[("Ideal", "own")]))
+    database.upsert_item(row(start_index=900, end_index=950, types=[("Ideal", "input")]))
+    assert len(database.search(types=["Ideal"], roles=["own"])) == 1
+    assert len(database.search(types=["Ideal"], roles=["input"])) == 1
+
+
+def test_search_by_page_finds_items_spanning_it(database: Database) -> None:
+    database.upsert_item(row(start_page=12, end_page=14))
+    assert len(database.search(page=13)) == 1
+    assert len(database.search(page=20)) == 0
+
+
+def test_dropping_a_page_range_lets_you_redo_part_of_a_book(database: Database) -> None:
+    database.upsert_item(row(start_page=12))
+    database.upsert_item(row(start_page=40, start_index=1, end_page=40, end_index=50))
+    removed = database.delete_pages("book-hash-a", 10, 20)
+    assert removed == 1
+    assert database.stats()["items"] == 1
+    assert database.search(page=40)
+
+
+def test_dropping_a_source_takes_its_items_with_it(database: Database) -> None:
+    database.upsert_item(row())
+    database.delete_source("book-hash-a")
+    assert database.stats()["items"] == 0
+    assert database.sources() == []
+
+
+def test_export_jsonl_leaves_out_bulk_by_default(database: Database, tmp_path: Path) -> None:
+    database.upsert_item(row())
+    out = tmp_path / "items.jsonl"
+    assert database.export_jsonl(out) == 1
+    record = json.loads(out.read_text(encoding="utf-8").splitlines()[0])
+    assert "source_text" not in record and "diagnostics" not in record
+    assert record["types"] == [{"name": "Int", "role": "input"}]
+    assert database.export_jsonl(out, include_source_text=True) == 1
+    assert "source_text" in json.loads(out.read_text(encoding="utf-8").splitlines()[0])
+
+
+def test_stats_counts_the_things_that_matter(database: Database) -> None:
+    database.upsert_item(row())
+    database.upsert_item(row(start_index=2, kind="problem", proved=False, verified=True))
+    stats = database.stats()
+    assert stats["items"] == 2 and stats["statements"] == 1 and stats["problems"] == 1
+    assert stats["verified"] == 2 and stats["proved"] == 1
+    assert database.type_counts()[0]["name"] == "Int"

tests/test_detect.py

@@ -0,0 +1,133 @@
+from __future__ import annotations
+
+from leanbench.detect import KIND_PROBLEM, KIND_STATEMENT, detect_document
+from leanbench.document import Document
+from leanbench.llm import ScriptedClient
+
+from .conftest import detection_reply
+
+
+def test_single_page_detection_reports_page_and_index(two_page_book: Document) -> None:
+    client = ScriptedClient(
+        [
+            detection_reply(
+                [
+                    {
+                        "kind": "statement",
+                        "label": "Definition 1.6.1",
+                        "summary": "divisibility",
+                        "start_quote": "Definition 1.6.1. Let a and b be integers.",
+                        "end_quote": "b = a k.",
+                        "continues_past_end": False,
+                    }
+                ]
+            ),
+            detection_reply([]),
+        ]
+    )
+    report = detect_document(client, two_page_book, max_window_pages=3)
+    assert len(report.detections) == 1
+    found = report.detections[0]
+    assert found.kind == KIND_STATEMENT
+    assert found.start_page == 1 and found.end_page == 1
+    page = two_page_book.page(1).text
+    assert page[found.start_index : found.end_index].startswith("Definition 1.6.1")
+    assert page[found.start_index : found.end_index].endswith("b = a k.")
+
+
+def test_item_running_off_the_page_triggers_a_second_page(two_page_book: Document) -> None:
+    truncated = detection_reply(
+        [
+            {
+                "kind": "statement",
+                "label": "Theorem 1.6.3",
+                "summary": "gcd exists",
+                "start_quote": "Theorem 1.6.3. Let a and b be nonzero integers.",
+                "end_quote": "the set of common",
+                "continues_past_end": True,
+            }
+        ]
+    )
+    whole = detection_reply(
+        [
+            {
+                "kind": "statement",
+                "label": "Theorem 1.6.3",
+                "summary": "gcd exists",
+                "start_quote": "Theorem 1.6.3. Let a and b be nonzero integers.",
+                "end_quote": "the greatest common divisor.",
+                "continues_past_end": False,
+            },
+            {
+                "kind": "problem",
+                "label": "Exercise 1.6.5",
+                "summary": "odd + odd is even",
+                "start_quote": "Exercise 1.6.5. Prove that the sum of two odd",
+                "end_quote": "odd integers is even.",
+                "continues_past_end": False,
+            },
+        ]
+    )
+    client = ScriptedClient([truncated, whole])
+    report = detect_document(client, two_page_book, max_window_pages=3)
+
+    assert len(client.calls) == 2, "the page should be re-read with its successor"
+    theorem = report.detections[0]
+    assert theorem.start_page == 1
+    assert theorem.end_page == 2, "the span must cross the page boundary"
+    assert theorem.spans_pages == 2
+    assert not theorem.truncated
+    assert two_page_book.page(2).text[: theorem.end_index].endswith("greatest common divisor.")
+
+    exercise = report.detections[1]
+    assert exercise.kind == KIND_PROBLEM
+    assert exercise.start_page == 2
+
+
+def test_window_stops_growing_at_the_limit_and_says_so(two_page_book: Document) -> None:
+    always_truncated = detection_reply(
+        [
+            {
+                "kind": "statement",
+                "label": "",
+                "summary": "",
+                "start_quote": "Definition 1.6.1. Let a and b be integers.",
+                "end_quote": "b = a k.",
+                "continues_past_end": True,
+            }
+        ]
+    )
+    client = ScriptedClient([always_truncated] * 4)
+    report = detect_document(client, two_page_book, max_window_pages=2)
+    assert len(client.calls) == 2
+    assert report.detections[0].truncated is True
+
+
+def test_unresolvable_quotes_are_recorded_not_invented(two_page_book: Document) -> None:
+    client = ScriptedClient(
+        [
+            detection_reply(
+                [
+                    {
+                        "kind": "statement",
+                        "label": "Hallucination 9",
+                        "summary": "not in the book",
+                        "start_quote": "Theorem 9.9.9 about topological quantum widgets",
+                        "end_quote": "which is absurd.",
+                        "continues_past_end": False,
+                    }
+                ]
+            ),
+            detection_reply([]),
+        ]
+    )
+    report = detect_document(client, two_page_book)
+    assert report.detections == []
+    assert len(report.unresolved) == 1
+
+
+def test_a_failing_page_does_not_kill_the_run(two_page_book: Document) -> None:
+    client = ScriptedClient(["not json at all", detection_reply([])])
+    report = detect_document(client, two_page_book)
+    assert report.pages_scanned == 2
+    assert any("detector failed" in u.get("reason", "") for u in report.unresolved)

tests/test_document.py

@@ -0,0 +1,46 @@
+from __future__ import annotations
+
+from leanbench.document import Document, Page, PageWindow, normalise_page_text
+
+
+def test_pages_are_numbered_from_one(two_page_book: Document) -> None:
+    assert len(two_page_book) == 2
+    assert [p.number for p in two_page_book.pages] == [1, 2]
+    assert two_page_book.page(1).text.startswith("Chapter 1")
+
+
+def test_window_locate_maps_back_to_the_right_page() -> None:
+    window = PageWindow([Page(7, "abcdef"), Page(8, "ghij")])
+    assert window.text == "abcdef\nghij"
+    assert window.locate(0) == (7, 0)
+    assert window.locate(5) == (7, 5)
+    assert window.locate(6) == (7, 6)      # end of page 7
+    assert window.locate(7) == (8, 0)      # first char of page 8
+    assert window.locate(10) == (8, 3)
+    assert window.locate(999) == (8, 4)    # clamped
+
+
+def test_window_globalise_is_the_inverse() -> None:
+    window = PageWindow([Page(1, "hello"), Page(2, "world")])
+    for page, offset in [(1, 0), (1, 4), (2, 0), (2, 4)]:
+        assert window.locate(window.globalise(page, offset)) == (page, offset)
+
+
+def test_document_slice_reconstructs_a_cross_page_span(two_page_book: Document) -> None:
+    page_one = two_page_book.page(1).text
+    start = page_one.index("Theorem 1.6.3")
+    end = two_page_book.page(2).text.index("has a greatest")
+    text = two_page_book.slice(1, start, 2, end)
+    assert text.startswith("Theorem 1.6.3")
+    assert text.rstrip().endswith("divisors of a and b")
+
+
+def test_normalisation_is_stable_and_gentle() -> None:
+    text = "first line   \nsecond"
+    assert normalise_page_text(text) == "first line\nsecond"
+    assert normalise_page_text(normalise_page_text(text)) == normalise_page_text(text)
+
+
+def test_page_checksum_changes_with_content() -> None:
+    assert Page(1, "a").checksum != Page(1, "b").checksum
+    assert Page(1, "a").checksum == Page(9, "a").checksum

tests/test_formalize.py

@@ -0,0 +1,90 @@
+from __future__ import annotations
+
+from leanbench.detect import KIND_PROBLEM, KIND_STATEMENT, Detection
+from leanbench.formalize import formalize, formalize_all, verification_mode
+from leanbench.llm import ScriptedClient
+from leanbench.verify import MODE_FULL, MODE_STATEMENT
+
+from .conftest import formalize_reply
+
+
+def make_detection(kind: str = KIND_STATEMENT) -> Detection:
+    return Detection(
+        kind=kind,
+        label="Theorem 1.6.2",
+        summary="divisibility is additive",
+        start_page=12,
+        start_index=100,
+        end_page=12,
+        end_index=260,
+        text="Theorem 1.6.2. If a divides b and a divides c then a divides b + c.",
+    )
+
+
+def test_open_problems_are_only_checked_as_statements() -> None:
+    assert verification_mode(make_detection(KIND_PROBLEM)) == MODE_STATEMENT
+    assert verification_mode(make_detection(KIND_STATEMENT)) == MODE_FULL
+
+
+def test_formalize_produces_verified_code_and_types(fake_checker) -> None:
+    client = ScriptedClient([formalize_reply()])
+    result = formalize(client, make_detection(), checker=fake_checker)
+    assert result.lean_code.startswith("theorem test_decl")
+    assert result.verified
+    assert not result.proved, "a sorry in the code means it is not proved"
+    assert ("Int", "input") in result.index_types
+
+
+def test_a_real_proof_counts_as_proved(fake_checker) -> None:
+    client = ScriptedClient(
+        [formalize_reply(lean_code="theorem t (n : Nat) : n = n := rfl", has_proof=True)]
+    )
+    result = formalize(client, make_detection(), checker=fake_checker)
+    assert result.has_proof and result.proved
+
+
+def test_lean_diagnostics_drive_a_repair_attempt(fake_checker) -> None:
+    client = ScriptedClient(
+        [
+            formalize_reply(lean_code="theorem t : BAD := by sorry"),
+            formalize_reply(lean_code="theorem t (n : Nat) : n = n := rfl", has_proof=True),
+        ]
+    )
+    result = formalize(client, make_detection(), checker=fake_checker, repair_attempts=1)
+    assert result.attempts == 2
+    assert result.verified
+    assert len(client.calls) == 2
+    repair_prompt = client.calls[1][-1]["content"]
+    assert "error: bad" in repair_prompt, "the compiler's own words go back to the model"
+
+
+def test_repair_gives_up_after_the_budget(fake_checker) -> None:
+    client = ScriptedClient([formalize_reply(lean_code="theorem t : BAD := by sorry")] * 3)
+    result = formalize(client, make_detection(), checker=fake_checker, repair_attempts=1)
+    assert result.attempts == 2
+    assert not result.verified
+
+
+def test_model_may_decline_an_unformalizable_passage(fake_checker) -> None:
+    client = ScriptedClient(['{"skip": true, "reason": "prose only"}'])
+    result = formalize(client, make_detection(), checker=fake_checker)
+    assert result.skipped and result.skip_reason == "prose only"
+    assert fake_checker.calls == []
+
+
+def test_imports_inside_the_body_are_stripped(fake_checker) -> None:
+    client = ScriptedClient(
+        [formalize_reply(lean_code="import Mathlib\ntheorem t (n : Nat) : n = n := rfl")]
+    )
+    result = formalize(client, make_detection(), checker=fake_checker)
+    assert "import" not in result.lean_code
+
+
+def test_one_bad_item_does_not_stop_the_batch(fake_checker) -> None:
+    client = ScriptedClient(["garbage, not json", formalize_reply()])
+    results = formalize_all(
+        client, [make_detection(), make_detection(KIND_PROBLEM)], checker=fake_checker
+    )
+    assert len(results) == 2
+    assert results[0].skipped and "formalizer failed" in results[0].skip_reason
+    assert results[1].verified

tests/test_llm.py

@@ -0,0 +1,38 @@
+from __future__ import annotations
+
+import pytest
+
+from leanbench.llm import LLMError, ScriptedClient, extract_code, parse_json
+
+
+def test_parse_json_plain() -> None:
+    assert parse_json('{"a": 1}') == {"a": 1}
+
+
+def test_parse_json_through_a_fence() -> None:
+    assert parse_json('```json\n{"a": [1, 2]}\n```') == {"a": [1, 2]}
+
+
+def test_parse_json_with_chatter_around_it() -> None:
+    assert parse_json('Sure!\n{"ok": true}\nHope that helps.') == {"ok": True}
+
+
+def test_parse_json_raises_when_there_is_none() -> None:
+    with pytest.raises(ValueError):
+        parse_json("no json here")
+
+
+def test_extract_code_pulls_the_lean_block() -> None:
+    raw = "Here you go:\n```lean4\ntheorem t : True := trivial\n```\nDone."
+    assert extract_code(raw) == "theorem t : True := trivial"
+
+
+def test_extract_code_passes_bare_code_through() -> None:
+    assert extract_code("theorem t : True := trivial") == "theorem t : True := trivial"
+
+
+def test_scripted_client_runs_out_loudly() -> None:
+    client = ScriptedClient(["one"])
+    assert client.complete([]) == "one"
+    with pytest.raises(LLMError):
+        client.complete([])

tests/test_ocr.py

@@ -0,0 +1,244 @@
+from __future__ import annotations
+
+from pathlib import Path
+
+import pytest
+
+from leanbench.document import Document
+from leanbench.ocr import (
+    OcrCache,
+    OcrReader,
+    VisionLLMBackend,
+    looks_broken,
+    text_quality,
+)
+
+# Real extraction of page 90 of the project's test book: the maths font carries a
+# custom encoding, so every operator arrives as a stray accent or ligature glyph.
+BROKEN = """Proposition 1.11.7 (Chinese remainder theorem). Let a and b be relatively
+prime natural numbers. There is an isomorphism of rings
+Zab Š Za ˚ Zb;
+defined by Œxab 7! .Œxa; Œxb/.
+"""
+
+# What the page actually says, as the vision model reads it.
+CLEAN = """Proposition 1.11.7 (Chinese remainder theorem). Let $a$ and $b$ be relatively
+prime natural numbers. There is an isomorphism of rings
+$$\\mathbb{Z}_{ab} \\cong \\mathbb{Z}_a \\oplus \\mathbb{Z}_b,$$
+defined by $[x]_{ab} \\mapsto ([x]_a, [x]_b)$.
+"""
+
+# The other corruption mode, from page 300 of the same book: the maths is made of
+# ordinary ASCII, so a glyph-based check scores it a perfect 1.0.
+OPERATORS_AS_LETTERS = """6.2.18. Let I and J be two ideals in a ring R. Show that
+I C J D fa C b W a 2 I and b 2 J g
+is an ideal in R.
+6.2.19. Let I and J be two ideals in a ring R. Show that
+IJ D fa1b1 C a2b2 C    C asbs W s  1; ai 2 I; bi 2 J g
+is an ideal in R, and IJ  I \\ J .
+"""
+
+PROSE = """The chapter closes with a discussion of why the theorem matters, and a
+remark on its history, with no displayed formulas at all.
+"""
+
+
+class FakeBackend:
+    """Returns a canned transcription and counts how often it was asked."""
+
+    name = "fake:v1"
+
+    def __init__(self, text: str = CLEAN) -> None:
+        self.text = text
+        self.calls = 0
+
+    def transcribe(self, image: bytes) -> str:
+        self.calls += 1
+        return self.text
+
+
+class ExplodingBackend:
+    name = "boom:v1"
+
+    def transcribe(self, image: bytes) -> str:
+        raise RuntimeError("model refused")
+
+
+# -- the quality heuristic -------------------------------------------------
+
+
+def test_mangled_maths_scores_far_below_clean_text() -> None:
+    assert text_quality(BROKEN) < 0.75
+    assert text_quality(CLEAN) > 0.9
+    assert text_quality(PROSE) > 0.9
+
+
+def test_operators_disguised_as_letters_are_caught() -> None:
+    """The failure mode that a glyph-only check scores 1.0 and waves through."""
+    assert text_quality(OPERATORS_AS_LETTERS) < 0.75
+    assert looks_broken(OPERATORS_AS_LETTERS)
+
+
+def test_ordinary_prose_with_numerals_survives() -> None:
+    assert not looks_broken(
+        "In chapter 2 we saw that the group has order 2 and index 2 in G.")
+
+
+def test_looks_broken_separates_the_two() -> None:
+    assert looks_broken(BROKEN)
+    assert not looks_broken(CLEAN)
+    assert not looks_broken(PROSE)
+
+
+def test_empty_text_is_the_worst_case() -> None:
+    assert text_quality("") == 0.0
+    assert text_quality("   \n  ") == 0.0
+
+
+def test_a_single_accented_word_is_not_damning() -> None:
+    # Real prose does contain the odd accent; only a pile of them is evidence.
+    assert not looks_broken("Consider the Poincare´ conjecture and its history.")
+
+
+# -- the cache -------------------------------------------------------------
+
+
+def test_cache_round_trips(tmp_path: Path) -> None:
+    cache = OcrCache(tmp_path)
+    assert cache.get("hash", 3, 200, "fake:v1") is None
+    cache.put("hash", 3, 200, "fake:v1", "hello")
+    assert cache.get("hash", 3, 200, "fake:v1") == "hello"
+    assert cache.hits == 1 and cache.misses == 1
+
+
+def test_cache_keys_on_dpi_and_backend(tmp_path: Path) -> None:
+    cache = OcrCache(tmp_path)
+    cache.put("hash", 3, 200, "fake:v1", "at 200")
+    assert cache.get("hash", 3, 400, "fake:v1") is None, "different dpi is a different read"
+    assert cache.get("hash", 3, 200, "other:v1") is None, "different backend too"
+
+
+def test_cache_can_be_switched_off(tmp_path: Path) -> None:
+    cache = OcrCache(tmp_path, enabled=False)
+    cache.put("hash", 1, 200, "fake:v1", "x")
+    assert cache.get("hash", 1, 200, "fake:v1") is None
+
+
+# -- the reader ------------------------------------------------------------
+
+
+def test_reader_pays_for_a_page_once(tmp_path: Path, monkeypatch) -> None:
+    monkeypatch.setattr("leanbench.ocr.render_page", lambda *a, **k: b"png")
+    backend = FakeBackend()
+    reader = OcrReader(backend=backend, cache=OcrCache(tmp_path))
+    first = reader.page_text("book.pdf", "hash", 7)
+    second = reader.page_text("book.pdf", "hash", 7)
+    assert first == second
+    assert backend.calls == 1, "the second read must come from cache"
+
+
+def test_reader_records_failures_instead_of_raising(tmp_path: Path, monkeypatch) -> None:
+    monkeypatch.setattr("leanbench.ocr.render_page", lambda *a, **k: b"png")
+    reader = OcrReader(backend=ExplodingBackend(), cache=OcrCache(tmp_path))
+    assert reader.page_text("book.pdf", "hash", 4) is None
+    assert "model refused" in reader.failures[4]
+
+
+def test_reader_strips_a_markdown_fence(tmp_path: Path, monkeypatch) -> None:
+    monkeypatch.setattr("leanbench.ocr.render_page", lambda *a, **k: b"png")
+    reader = OcrReader(backend=FakeBackend("```\nTheorem 1.\n```"), cache=None)
+    assert reader.page_text("book.pdf", "hash", 1) == "Theorem 1."
+
+
+# -- the vision backend's request shape ------------------------------------
+
+
+def test_vision_backend_sends_an_image_part() -> None:
+    captured: dict = {}
+
+    class Client:
+        def complete(self, messages, **kwargs):
+            captured["messages"] = messages
+            captured["kwargs"] = kwargs
+            return "  transcribed  "
+
+    backend = VisionLLMBackend(client=Client(), model="qwen-vl-max")
+    assert backend.transcribe(b"\x89PNG") == "transcribed"
+    parts = captured["messages"][0]["content"]
+    assert parts[0]["type"] == "text"
+    assert parts[1]["type"] == "image_url"
+    assert parts[1]["image_url"]["url"].startswith("data:image/png;base64,")
+    assert captured["kwargs"]["model"] == "qwen-vl-max"
+    assert backend.name == "vision:qwen-vl-max"
+
+
+# -- Document integration --------------------------------------------------
+
+
+@pytest.fixture()
+def mixed_book(tmp_path: Path) -> Path:
+    """Page 1 is fine, page 2 is font-mangled."""
+    path = tmp_path / "mixed.txt"
+    path.write_text(PROSE + "\f" + BROKEN, encoding="utf-8")
+    return path
+
+
+def test_auto_mode_only_pays_for_the_broken_page(mixed_book: Path, monkeypatch) -> None:
+    monkeypatch.setattr("leanbench.ocr.render_page", lambda *a, **k: b"png")
+    backend = FakeBackend()
+    reader = OcrReader(backend=backend, cache=None)
+    document = Document.load(mixed_book, mode="auto", ocr=reader, threshold=0.75)
+
+    assert backend.calls == 1, "the clean page must not be sent to the model"
+    assert document.meta["ocr"]["pages_replaced"] == [2]
+    assert document.page(1).text.startswith("The chapter closes")
+    assert "\\cong" in document.page(2).text
+    assert "fake:v1" in document.extractor
+
+
+def test_ocr_mode_reads_every_page(mixed_book: Path, monkeypatch) -> None:
+    monkeypatch.setattr("leanbench.ocr.render_page", lambda *a, **k: b"png")
+    backend = FakeBackend()
+    Document.load(mixed_book, mode="ocr", ocr=reader_for(backend))
+    assert backend.calls == 2
+
+
+def reader_for(backend) -> OcrReader:
+    return OcrReader(backend=backend, cache=None)
+
+
+def test_page_range_bounds_what_gets_read(mixed_book: Path, monkeypatch) -> None:
+    monkeypatch.setattr("leanbench.ocr.render_page", lambda *a, **k: b"png")
+    backend = FakeBackend()
+    document = Document.load(mixed_book, mode="ocr", ocr=reader_for(backend),
+                             first_page=2, last_page=2)
+    assert backend.calls == 1, "a 25-page trial of a 600-page book costs 25 calls"
+    assert document.meta["ocr"]["pages_replaced"] == [2]
+
+
+def test_text_mode_never_touches_the_model(mixed_book: Path) -> None:
+    backend = FakeBackend()
+    document = Document.load(mixed_book, mode="text", ocr=reader_for(backend))
+    assert backend.calls == 0
+    assert "Š" in document.page(2).text, "embedded text is left exactly as found"
+    assert "ocr" not in document.meta
+
+
+def test_a_failed_page_keeps_its_embedded_text(mixed_book: Path, monkeypatch) -> None:
+    monkeypatch.setattr("leanbench.ocr.render_page", lambda *a, **k: b"png")
+    reader = OcrReader(backend=ExplodingBackend(), cache=None)
+    document = Document.load(mixed_book, mode="ocr", ocr=reader)
+    assert document.meta["ocr"]["pages_failed"] == [1, 2]
+    assert "Š" in document.page(2).text, "we fall back, we do not lose the page"
+
+
+def test_offsets_stay_usable_after_ocr(mixed_book: Path, monkeypatch) -> None:
+    """The span contract must hold whichever extractor produced the text."""
+    monkeypatch.setattr("leanbench.ocr.render_page", lambda *a, **k: b"png")
+    document = Document.load(mixed_book, mode="ocr", ocr=reader_for(FakeBackend()))
+    page = document.page(2)
+    start = page.text.index("Proposition")
+    end = page.text.index("rings") + len("rings")
+    assert document.slice(2, start, 2, end).startswith("Proposition 1.11.7")
+    # The extractor is part of the offset contract, so it is recorded on the source.
+    assert "fake:v1" in document.extractor

tests/test_pipeline.py

@@ -0,0 +1,158 @@
+from __future__ import annotations
+
+from pathlib import Path
+
+from leanbench.config import Settings
+from leanbench.db import Database
+from leanbench.document import Document
+from leanbench.llm import ScriptedClient
+from leanbench.pipeline import ingest
+
+from .conftest import detection_reply, formalize_reply
+
+DETECT_PAGE_ONE = detection_reply(
+    [
+        {
+            "kind": "statement",
+            "label": "Definition 1.6.1",
+            "summary": "divisibility",
+            "start_quote": "Definition 1.6.1. Let a and b be integers.",
+            "end_quote": "b = a k.",
+            "continues_past_end": False,
+        },
+        {
+            "kind": "statement",
+            "label": "Theorem 1.6.3",
+            "summary": "gcd exists",
+            "start_quote": "Theorem 1.6.3. Let a and b be nonzero integers.",
+            "end_quote": "the set of common",
+            "continues_past_end": True,
+        },
+    ]
+)
+
+DETECT_BOTH_PAGES = detection_reply(
+    [
+        {
+            "kind": "statement",
+            "label": "Definition 1.6.1",
+            "summary": "divisibility",
+            "start_quote": "Definition 1.6.1. Let a and b be integers.",
+            "end_quote": "b = a k.",
+            "continues_past_end": False,
+        },
+        {
+            "kind": "statement",
+            "label": "Theorem 1.6.3",
+            "summary": "gcd exists",
+            "start_quote": "Theorem 1.6.3. Let a and b be nonzero integers.",
+            "end_quote": "the greatest common divisor.",
+            "continues_past_end": False,
+        },
+        {
+            "kind": "problem",
+            "label": "Exercise 1.6.4",
+            "summary": "mutual divisibility",
+            "start_quote": "Exercise 1.6.4. Show that if a divides b and b divides a",
+            "end_quote": "a = b or a = -b.",
+            "continues_past_end": False,
+        },
+    ]
+)
+
+
+def _settings(tmp_path: Path) -> Settings:
+    settings = Settings.from_env(dotenv=None)
+    settings.database = str(tmp_path / "leanbench.sqlite")
+    settings.repair_attempts = 0
+    return settings
+
+
+def test_end_to_end_run_stores_indexed_items(tmp_path: Path, two_page_book, fake_checker) -> None:
+    client = ScriptedClient(
+        [DETECT_PAGE_ONE, DETECT_BOTH_PAGES]
+        + [
+            formalize_reply(name="divides_def",
+                            lean_code="def divides (a b : Int) : Prop := ∃ k : Int, b = a * k"),
+            formalize_reply(name="gcd_exists",
+                            lean_code="theorem gcd_exists (a b : Int) : True := by\n  sorry"),
+            formalize_reply(name="dvd_antisymm'",
+                            lean_code="theorem dvd_antisymm' (a b : Int) : True := by\n  sorry"),
+        ]
+    )
+    settings = _settings(tmp_path)
+    database = Database(settings.database)
+    result = ingest(
+        two_page_book.path,
+        settings=settings,
+        client=client,
+        database=database,
+        checker=fake_checker,
+        title="Test Book",
+    )
+    summary = result.summary()
+    assert summary["detected"] == 3
+    assert summary["problems"] == 1
+    assert summary["multi_page"] == 1
+    assert summary["stored"] == 3
+    assert summary["verified"] == 3
+
+    assert database.stats()["items"] == 3
+    by_type = database.search(types=["Int"])
+    assert len(by_type) == 3, "every item is reachable through its types"
+    problems = database.search(kind="problem")
+    assert len(problems) == 1 and problems[0]["start_page"] == 2
+    database.close()
+
+
+def test_reingesting_a_page_range_replaces_only_that_range(
+    tmp_path: Path, two_page_book: Document, fake_checker
+) -> None:
+    settings = _settings(tmp_path)
+    database = Database(settings.database)
+
+    first = ScriptedClient([DETECT_PAGE_ONE, DETECT_BOTH_PAGES] + [formalize_reply()] * 3)
+    ingest(two_page_book.path, settings=settings, client=first, database=database,
+           checker=fake_checker)
+    assert database.stats()["items"] == 3
+
+    # redo page 2 only: the page-1 item survives, page-2 items are rebuilt
+    second = ScriptedClient(
+        [
+            detection_reply(
+                [
+                    {
+                        "kind": "problem",
+                        "label": "Exercise 1.6.5",
+                        "summary": "odd plus odd",
+                        "start_quote": "Exercise 1.6.5. Prove that the sum of two odd",
+                        "end_quote": "odd integers is even.",
+                        "continues_past_end": False,
+                    }
+                ]
+            ),
+            formalize_reply(name="odd_add_odd"),
+        ]
+    )
+    ingest(two_page_book.path, settings=settings, client=second, database=database,
+           checker=fake_checker, first_page=2, last_page=2)
+
+    pages = sorted(item["start_page"] for item in database.search(limit=100))
+    assert pages == [1, 1, 2], "page 1 untouched, page 2 replaced by the new run"
+    database.close()
+
+
+def test_a_run_without_lean_stores_items_but_claims_nothing(
+    tmp_path: Path, two_page_book: Document
+) -> None:
+    from leanbench.verify import NullChecker
+
+    client = ScriptedClient([DETECT_PAGE_ONE, DETECT_BOTH_PAGES] + [formalize_reply()] * 3)
+    settings = _settings(tmp_path)
+    database = Database(settings.database)
+    result = ingest(two_page_book.path, settings=settings, client=client, database=database,
+                    checker=NullChecker())
+    assert result.summary()["stored"] == 3
+    assert result.summary()["verified"] == 0
+    assert database.search(verified=True) == []
+    database.close()

tests/test_typeindex.py

@@ -0,0 +1,81 @@
+from __future__ import annotations
+
+from leanbench.typeindex import ROLE_GOAL, ROLE_INPUT, ROLE_OWN, index_types, parse_signature
+
+
+def test_theorem_is_indexed_by_the_types_of_its_inputs() -> None:
+    code = "theorem add_dvd (a b c : Int) (h : a ∣ b) (k : a ∣ c) : a ∣ b + c := by\n  sorry"
+    signature = parse_signature(code)
+    assert signature is not None
+    assert signature.is_proof
+    assert signature.name == "add_dvd"
+    assert "Int" in signature.inputs
+    pairs = index_types(code)
+    assert ("Int", ROLE_INPUT) in pairs
+
+
+def test_definition_is_indexed_by_its_own_type() -> None:
+    code = "def divides (a b : Int) : Prop := ∃ k : Int, b = a * k"
+    signature = parse_signature(code)
+    assert signature is not None
+    assert not signature.is_proof
+    pairs = index_types(code)
+    assert ("Int", ROLE_INPUT) in pairs
+    assert ("Prop", ROLE_OWN) in pairs, "a predicate's own type is the point of it"
+    assert all(role != ROLE_GOAL for _, role in pairs)
+
+
+def test_a_proof_is_not_indexed_by_Prop() -> None:
+    pairs = index_types("theorem t (n : Nat) : n = n := rfl")
+    assert all(name != "Prop" for name, _ in pairs)
+
+
+def test_definition_of_a_concrete_type_records_it() -> None:
+    pairs = index_types("def double (n : Nat) : Nat := 2 * n")
+    assert ("Nat", ROLE_OWN) in pairs
+
+
+def test_instance_binders_count_as_inputs() -> None:
+    code = "theorem foo {G : Type*} [Group G] (x : G) : x * 1 = x := by simp"
+    signature = parse_signature(code)
+    assert signature is not None
+    assert "Group" in signature.inputs
+
+
+def test_unicode_number_types_are_normalised() -> None:
+    code = "theorem sq_nonneg' (n : ℤ) : 0 ≤ n ^ 2 := by positivity"
+    pairs = dict(index_types(code))
+    assert pairs.get("Int") == ROLE_INPUT
+
+
+def test_structure_records_its_own_type() -> None:
+    code = "structure Monoid' (M : Type) : Type where\n  one : M"
+    signature = parse_signature(code)
+    assert signature is not None
+    assert signature.keyword == "structure"
+    assert signature.own or signature.inputs
+
+
+def test_model_supplied_types_are_merged_without_duplicates() -> None:
+    code = "theorem t (n : Nat) : n = n := rfl"
+    pairs = index_types(code, ["Nat", "Polynomial", "  "])
+    names = [name for name, _ in pairs]
+    assert names.count("Nat") == 1
+    assert "Polynomial" in names
+
+
+def test_comments_do_not_leak_into_the_index() -> None:
+    code = "-- about Matrix stuff\n/- Group -/\ntheorem t (n : Nat) : n = n := rfl"
+    names = [name for name, _ in index_types(code)]
+    assert "Matrix" not in names and "Group" not in names
+
+
+def test_declaration_keyword_detected_after_attributes() -> None:
+    code = "@[simp]\nprivate theorem t (n : Nat) : n = n := rfl"
+    signature = parse_signature(code)
+    assert signature is not None and signature.keyword == "theorem"
+
+
+def test_unparsable_code_yields_nothing_rather_than_nonsense() -> None:
+    assert parse_signature("this is not lean") is None
+    assert index_types("this is not lean") == []