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`
  + `database/goodman-1.6.index.jsonl`): 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. 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 \
  --out-index database/goodman-1.6.index.jsonl \
  --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. Then query it with the current goal:

```sh
python3 textbook/search_database.py database/goodman-1.6.index.jsonl \
  "\u22a2 Nat.Prime p \u2192 (p:\u2124) \u2223 List.prod as \u2192 \u2203 a \u2208 as, (p:\u2124) \u2223 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.