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 library candidates** (`library_candidates/goodman-1.6.jsonl`): the book's
  stated Theorem/Proposition/Lemma/Corollary claims from the section's main text.
  These are NOT bench targets -- they are premises waiting to be proven once and
  then reused, the way Mathlib itself is a library of already-proven facts an agent
  can cite while proving something new. An entry only belongs in the trustworthy,
  reusable library after `lean-bench` has actually proven it for real (see step 5);
  `build_library.py` already enforces this -- it only assembles entries whose
  `results.jsonl` says `success: true`, with the exact proof that was checked, never
  anything from this file directly.
- **Definitions** (`textbook/*.definitions.json` + `lib/Definitions.lean`): a
  concept a bench/library statement depends on. When Mathlib already has it
  (`mathlib_ref` set), statements just use that name directly. When it doesn't
  (`mathlib_ref: null`), the manifest also carries real, hand-written Lean code
  (`lean_code`), compiled by `build_definitions.py` into an actual importable
  `.lean` file -- Lean can only ever verify a proof about a concept that exists as
  real Lean code somewhere, a JSON description of a definition is not enough for it
  to typecheck anything that mentions it.

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 library_candidates/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 library_candidates/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. Assemble proven library candidates into a reusable library file

```sh
python3 textbook/build_library.py library_candidates/goodman-1.6.jsonl \
  results/goodman-1.6-001-library/results.jsonl --out lib/Chapter01Section06.lean
```

(This step needs its own `lean-bench` run over `library_candidates/`, proving those
statements the same way step 5 proves the exercises -- not yet done for section
1.6.) Only entries that were actually proven in that run go in, with the exact
proof that was checked, verbatim. Later chapters `import` this file to build on
already-proven results -- it's one flat `.lean` file, not a real Lake
package/module boundary.

## 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.