Book formalizer

Converts an OCR'd mathematics book (Markdown) into a clean, per-section Markdown collection plus structured JSON for downstream Isabelle/HOL autoformalization.

Hand-edits before running

Strip cover, preface, acknowledgements, and TOC/index. The book should begin at # Chapter 1. These are marked keep=false downstream anyway, but pre-trimming speeds up stage 1.

Pipeline

Stage	Script	Output
1	segment.py	01_classified.json — blocks typed, labelled, deps + notation extracted
2	notation.py	02_notation.json — flattened notation table
3	normalize.py	03_normalized.json — LaTeX standardised, filler stripped
4	assemble.py	sections/*.md, definitions.md, deps.json, notation.json, proofs.json

Usage

make all INPUT=input/boools.md     # full run
make stage1-test                   # quick run on input/test.md
make dry                           # NO_LLM=1 smoke test
make clean

Requires DASHSCOPE_API_KEY (Qwen 3.6 plus). Managed with uv, type-checked with ty.

Env vars

• FORCE=1 — overwrite existing intermediate output
• NO_LLM=1 — skip LLM calls (dry run)
• MAX_WORKERS — parallel LLM threads (default 8)
• CHUNK_CHAR_CEILING — stage-1 chunk size (default 20000)
• SPLIT_DEPTH — stage-4 section-split heading depth (default 2)

Outputs

• output/sections/NN_<slug>.md — one file per top-level section.
• output/definitions.md — all definitions, labelled.
• output/deps.json — cross-reference graph, keyed by section → label.
• output/notation.json — symbol table {block_id, label, symbol, reads, kind, section}.
• output/proofs.json — flat array of {label, statement_id, proof_id, section, statement, proof} pairing each formal result with its informal proof.

Open issues

See OPEN_PROBLEMS.md.