lean-bench/textbook/README.md

# Textbook formalization pipeline

Turns one book (currently Goodman, *Algebra: Abstract and Concrete*) into two
distinct things `lean-bench`/`lean-agent` can use, not one:

- **The bench** (`datasets/goodman-1.6-exercises.jsonl`): real problems the reader
  is meant to solve, sourced from the book's own **Exercises** at the end of each
  section. These are the actual targets `lean-bench` scores an agent against.
- **The database** (`database/goodman-1.6.jsonl` -> `lib/Goodman/Chapter01Section06.lean`):
  the book's stated Theorem/Proposition/
  Lemma/Corollary claims from the main text, turned by `build_database.py` into real
  Lean declarations an agent can **cite by name** while proving a bench target --
  the "third party math library" role Mathlib plays, except scoped to this book.
  You do not re-prove Mathlib's theorems to use them, and the same applies here: the
  book proves its own body results, and its exercises are posed assuming them. So an
  entry is emitted as an `axiom` (asserted from the textbook) until a real
  `lean-bench` run proves it, at which point `--results` upgrades it to a
  `theorem` carrying the exact proof that was verified.

  The cost of that shortcut is real and worth stating plainly: anything proven
  *through* an axiom inherits it, so a garbled extraction asserted as an axiom can
  make downstream "proofs" worthless. Two guards: `--require-checked` refuses any
  entry that hasn't passed `check_statements.py`, and the verifier's
  `#print axioms` check surfaces what a finished proof actually rests on. Every
  axiom here still needs a human to have read it against the book.
- **Retrieval** (`search_database.py`): given the current goal, ranks database
  premises by identifier/symbol overlap with rare identifiers weighted higher, and
  formats the top few for the LLM prompt. It reads the database JSONL directly and
  derives each premise's declaration name, identifiers and proof status itself
  (sharing those functions with `build_database.py`), so the data exists in exactly
  one place. There is deliberately no generated index: at this scale deriving them
  costs microseconds, and a second copy that nothing checks for freshness could
  silently serve statements that no longer match the `.lean` file. An index earns
  its place once it holds something actually expensive, i.e. embeddings. This is the step the proof loop calls at
  each line -- it narrows ~20 premises to the few worth showing, and cannot tell you
  whether one applies; only Lean can. Swapping in embeddings later means replacing
  `score_premise()` and nothing else.
- **Definitions** (`textbook/*.definitions.json` + `lib/Definitions.lean`): a concept
  a statement depends on. When Mathlib has it (`mathlib_ref` set), statements use
  that name directly. When it doesn't (`mathlib_ref: null`), the manifest carries
  real hand-written Lean (`lean_code`), compiled by `build_definitions.py` into an
  importable `.lean` file -- Lean can only verify a proof about a concept that
  exists as real Lean code, a JSON description of a definition is not enough.

This pipeline does not itself prove anything or run Lean; see "What this pipeline
does not do" below and `lean-agent`'s own README for how proving actually happens
(goal-directed proof search against the library, not a single-shot proof attempt --
see "How this is meant to connect to lean-agent" at the end of this file).

## What this pipeline does not do

- Does not produce proofs. Every `statement` field is an unproven target; a Lean
  `sorry` would technically "complete" it, which is exactly why proving is left to
  `lean-agent`/`lean-bench`, not this pipeline.
- Does not verify Lean statements type-check inside the Cowork sandbox -- there is
  no Lean/Lake/Mathlib there (also architecturally incompatible: your local
  `~/.elan` has macOS binaries, the sandbox is a Linux VM). `check_statements.py`
  must run on your machine against a Mathlib-backed Lean project; see "Local
  environment setup" below.
- Does not commit the textbook PDF or large raw/derived full-text extraction dumps
  to git -- `.gitignore` excludes `*.pdf` and `textbook/*.txt`, since that's
  copyrighted material that should only ever live on your machine. Only code, the
  generated JSON/JSONL datasets (short Lean statements + your own short English
  glosses), and the compiled `Definitions.lean` go into git.

## Usage

### 1. Extract one chapter's layout text from the PDF

```sh
pdftotext -layout -f <start pdf page> -l <end pdf page> uiowa-algebra.pdf textbook/chapterNN_layout.txt
```

Check page numbers with `pdfinfo`/`pypdf` first -- the book's printed page numbers
and the PDF's physical page numbers differ (front matter, table of contents).

### 2. Slice out a section's body and its exercises separately

```sh
python3 textbook/extract_section.py textbook/chapterNN_layout.txt \
  --start-heading "1.6. Divisibility in the Integers" \
  --end-heading "1.7. Modular Arithmetic" \
  --section-prefix "1.6." \
  --out-text textbook/section_1_6.txt \
  --out-index textbook/section_1_6.index.json

python3 textbook/extract_exercises.py textbook/chapterNN_layout.txt \
  --start-heading "Exercises 1.6" \
  --end-heading "1.7. Modular Arithmetic" \
  --section-prefix "1.6." \
  --out-text textbook/exercises_1_6.txt \
  --out-index textbook/exercises_1_6.index.json
```

Headings must match the layout text's own section-title lines **verbatim**.
`extract_exercises.py` drops obvious false positives (a sentence like "...converse
of Proposition\n1.6.19." can wrap so the bare number lands alone at a line start,
looking exactly like a real exercise heading) -- anything dropped is printed to
stderr, never silently lost.

### 3. Formalize the body (-> library candidates) and the exercises (-> bench) separately

```sh
export DASHSCOPE_API_KEY=...   # or put it in lean-bench/.env (gitignored)

python3 textbook/formalize.py \
  textbook/section_1_6.txt textbook/section_1_6.index.json \
  --model qwen-max --base-url https://dashscope.aliyuncs.com/compatible-mode/v1 \
  --out-dataset database/goodman-1.6.jsonl \
  --out-definitions textbook/goodman-1.6.definitions.json \
  --out-excluded textbook/goodman-1.6.excluded.jsonl

python3 textbook/formalize_exercises.py \
  textbook/section_1_6.txt textbook/exercises_1_6.txt textbook/exercises_1_6.index.json \
  --model qwen-max --base-url https://dashscope.aliyuncs.com/compatible-mode/v1 \
  --out-dataset datasets/goodman-1.6-exercises.jsonl \
  --out-excluded textbook/goodman-1.6-exercises.excluded.jsonl
```

`formalize_exercises.py` is given the body text too, because many exercises say
things like "Prove Proposition 1.6.9" instead of restating the claim -- the model
needs the body to know what that actually says, and is told to write out the full
claim, never a placeholder like "the statement of Proposition 1.6.9".

Both steps validate that every checklist item is covered by at least one output
entry (included or explicitly excluded with a reason) and raise an error if the
model silently drops one instead -- this caught a real bug during the exercises
pilot (7 of 15 checklist items were dropped with no trace on the first attempt).

The source PDF's math symbol extraction is unreliable (missing/garbled ≡, ∈,
superscripts), so this step leans on the model's own knowledge of standard textbook
mathematics rather than literal transcription. Candidate statements must go through
step 4 before you trust them -- in practice, even after that, expect to still need
to read and fix a meaningful fraction by hand (both the exercises and the original
body pilot needed real fixes to type mismatches, invalid syntax, and even one
mathematically false claim smuggled in as a "prove or disprove" exercise that got
mis-included as an unconditional theorem).

### 4. Check candidate statements type-check on your machine

```sh
python3 textbook/check_statements.py database/goodman-1.6.jsonl \
  --lean-project /path/to/your/mathlib-project \
  --lean-command '["lake","env","lean"]' \
  --report textbook/goodman-1.6.elab-report.jsonl

python3 textbook/check_statements.py datasets/goodman-1.6-exercises.jsonl \
  --lean-project /path/to/your/mathlib-project \
  --lean-command '["lake","env","lean"]' \
  --report textbook/goodman-1.6-exercises.elab-report.jsonl
```

This only checks "does this Lean statement type-check" (via `sorry`), not "is it
provable" or "is it faithful to the book" -- report any `FAIL` id and its Lean
diagnostics and they'll get fixed and pushed back.

### 5. Prove the bench targets for real with lean-agent/lean-bench

```sh
lean-bench datasets/goodman-1.6-exercises.jsonl --output results/goodman-1.6-001 \
  --lean-project /path/to/your/mathlib-project --lean-command '["lake","env","lean"]' \
  --model ... --base-url ...
```

### 6. Compile hand-written definitions into real, importable Lean

```sh
python3 textbook/build_definitions.py textbook/goodman-1.6.definitions.json --out lib/Definitions.lean
```

Only definitions with no Mathlib equivalent (`mathlib_ref: null`) contribute
anything here -- everything else is used directly by name. Any statement whose
`prelude` needs one of these also inlines the `def` itself (self-contained per
task, matching how `check_statements.py` elaborates one task at a time), so
`lib/Definitions.lean` is the single canonical copy and the inlined ones must stay
in sync with it by construction (generated from the same manifest).

### 7. Verify recorded proofs

A database entry may carry a `proof` (hand-written, or authored by an agent outside
a bench run), but it stays an `axiom` until Lean compiles it -- an unverified proof
never upgrades an entry, so the library cannot claim more than Lean confirmed.

```sh
python3 textbook/check_proofs.py database/goodman-1.6.jsonl \
  --lean-project /path/to/your/mathlib-project \
  --lean-command '["lake","env","lean"]' \
  --report textbook/goodman-1.6.proof-report.jsonl \
  --update
```

Stricter than check_statements.py: it compiles `theorem ... := by <proof>`, rejects
`sorry`/`admit`/`native_decide`, and reads `#print axioms` to reject a proof that
depends on anything beyond Lean's own three axioms -- notably one that leans on a
book-asserted `axiom` from this very database, which would not be an independent
proof. `--update` writes `proof_checked` back, which is what promotes an entry on
the next build.

### 8. Generate the citable premise database

```sh
python3 textbook/build_database.py database/goodman-1.6.jsonl \
  --out-lean lib/Goodman/Chapter01Section06.lean \
  --require-checked
```

Add `--results results/goodman-1.6-library-001/results.jsonl` once a `lean-bench`
run over `database/goodman-1.6.jsonl` has proven some of them, to upgrade those
entries from `axiom` to real theorems. Query it with the current goal:

```sh
python3 textbook/search_database.py database/goodman-1.6.jsonl \
  "⊢ Nat.Prime p → (p:ℤ) ∣ List.prod as → ∃ a ∈ as, (p:ℤ) ∣ a"
```

(`build_library.py` predates this and remains for the narrower job of assembling
*only* proven entries with no axioms at all; note it attaches each entry's
non-import prelude per-theorem, which would emit a shared `def` twice in one file --
`build_database.py` hoists and dedupes them instead.)

## How this is meant to connect to lean-agent

This pipeline only produces data files; it is not the proof search itself. The
intended `lean-agent` workflow this feeds:

1. Given a target statement, check whether it's even valid Lean (this is what
   `check_statements.py` does ahead of time, so `lean-agent` doesn't waste attempts
   on a statement that can't type-check no matter what).
2. Track the current proof state as a list of open goals (the same thing the
   [vscode-lean4](https://github.com/leanprover/vscode-lean4) plugin shows you
   live) -- not attempt the whole theorem in one LLM call.
3. At each step, search a database of already-proven statements (`lib/*.lean`,
   built by `build_library.py`, plus Mathlib itself) for something applicable to
   the current goal -- the equivalent of Lean's `exact?`/`apply?` tactics, or a
   semantic/embedding search over the library -- and if something is used, apply it
   and fold the resulting subgoals back into the open-goals list.
3. Repeat until the goal list is empty (theorem proved) or a budget is exhausted
   (forced stop, left as an open goal / `sorry`).

That proof-search loop isn't built yet -- `lean-bench`'s current `solve()` call is
still single-shot (one LLM call, checked by Lean, retried up to `--attempts` times
from scratch), not goal-directed. This pipeline's two-track split (bench targets
from exercises, growing library from proven body content) is what that loop will
need once it exists.

## Local environment setup: a Lake project with Mathlib

The Cowork sandbox has no Lean; `check_statements.py` and real `lean-agent`/
`lean-bench` runs both need to happen on your machine (or anywhere else with Lean).
If you don't have such a project yet:

```sh
cd ~/ProjectResearch   # anywhere
lake +leanprover/lean4:v4.33.1 new mathlib-bench math
cd mathlib-bench
lake exe cache get     # downloads Mathlib's precompiled cache -- much faster than building from source
lake build Mathlib     # compiles Mathlib's own top-level .olean aggregator (cache get alone doesn't)
```

Then point `--lean-project` at `mathlib-bench` and `--lean-command` at
`'["lake","env","lean"]'`.

## Feedback loop

I (claude-bot) generate/edit files in ProjectResearch -> commit and push to
`Zayden-Jung/lean-bench` (using claude-bot's token) -> you `git pull` locally ->
run `check_statements.py` / `lean-bench` -> send back the failing ids and Lean's
diagnostics -> I fix and push again. Ordinary git round-trip, no extra tooling.