# Textbook formalization pipeline 把一本教科书（目前是 Goodman, *Algebra: Abstract and Concrete*）里正文的 Theorem/Proposition/Lemma/Corollary 转成 lean-bench 能跑的任务 JSONL，配套 Definition 清单（优先复用 Mathlib，Mathlib 没有的才手写），再由 lean-agent 在 一个真正带 Mathlib 的 Lean 项目里验证/证明。这条流水线本身不跑 Lean，也不联网 以外没有第三方依赖。 ## 这条流水线不做什么 - 不产出证明。生成的只是**待证命题**（`statement` 字段），证明留给 `lean-agent`/`lean-bench` 去跑。 - 不在 Cowork 沙盒里验证 Lean 语句能不能通过类型检查——沙盒里没有装 Lean/Lake/Mathlib（架构也不兼容：本机 `~/.elan` 下是 macOS 二进制，沙盒是 Linux VM，跑不了），所以 `check_statements.py` 必须在你本机、且是一个已经 `lake exe cache get` 过的 Mathlib 项目里跑，见下面"本机环境准备"。 - 不会把教科书 PDF 或者大段原文提取结果提交进 git——`.gitignore` 里已经排除 了 `*.pdf` 和 `textbook/*.txt`，这些是版权内容，只应该留在你本机。只有代码、 生成的最终数据集（短的 Lean 语句 + 自己改写的简短英文释义）会进仓库。 ## 用法 ### 1. 从 PDF 提取一章的版式文本 ```sh pdftotext -layout -f <起始pdf页码> -l <结束pdf页码> uiowa-algebra.pdf textbook/chapterNN_layout.txt ``` 页码用 `pdfinfo`/`pypdf` 先核对——书里印的页码和 PDF 物理页码不是一回事（前 面有目录、序言）。 ### 2. 切出一个 section，列出带编号的条目清单 ```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 ``` `--start-heading`/`--end-heading` 必须和版式文本里独占一行的章节标题**逐字** 一致（提取时打印出的书本身的标题行）；`--end-heading` 留空就切到文件末尾。 输出的 index JSON 是这个 section 里所有 `Theorem/Proposition/Lemma/ Corollary/Definition N.N.N` 开头的条目清单（自动去重了跨页重复的标签），用来 让下一步的 LLM 不漏项、不编项目。 ### 3. 用 LLM 把 section 形式化成候选 Lean 语句 ```sh export DASHSCOPE_API_KEY=... # 或者写进 lean-bench/.env（已 gitignore） 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 datasets/goodman-1.6.jsonl \ --out-definitions textbook/goodman-1.6.definitions.json \ --out-excluded textbook/goodman-1.6.excluded.jsonl ``` 模型会为每条 Theorem/Proposition/Lemma/Corollary 产出一个 Lean 4 命题 （`statement`）、需要的 `prelude`（通常就是 `import Mathlib`）、一句自己改写 的英文释义，以及用到的 Mathlib 标识符列表；为每条相关的 Definition 产出一个 清单条目——如果 Mathlib 已经有对应概念（`mathlib_ref` 非空）就不写 Lean 代 码，只有 Mathlib 没有的概念才会给出手写的 `def`。判断这条目根本没法形式化 （纯计算题、内容太模糊/被 PDF 提取污染到读不出原意）的条目，会带着 `include_in_bench: false` 和原因单独写进 `--out-excluded`，不会进真正的数据 集，但也不会被静默丢弃——都留痕方便你复核。 源 PDF 的数学符号提取质量很差（≡、∈、上下标经常丢失或乱码），这一步依赖模 型自己对标准教材内容的知识去猜测/还原真实含义，**不是逐字翻译提取出来的文 本**。所以生成的候选语句必须经过下一步验证，不能直接信。 ### 4. 在你本机验证候选语句能不能通过类型检查 见下面"本机环境准备"先搭好一个带 Mathlib 的 Lake 项目，然后： ```sh python3 textbook/check_statements.py datasets/goodman-1.6.jsonl \ --lean-project /path/to/your/mathlib-project \ --lean-command '["lake","env","lean"]' \ --report textbook/goodman-1.6.elab-report.jsonl ``` 这一步只检查"这句 Lean 能不能通过类型检查"（用 `sorry` 占位），**不检查证明 是否存在、也不检查是否忠实于原书**——分别对应两件不同的事：语法/引用是否正 确，跟数学内容是否正确。失败的条目（`FAIL`）要么是模型编造了不存在的 Mathlib 标识符，要么是语句本身写错了，需要你告诉我具体哪条、Lean 报的什么 错，我再改。 ### 5. 用 lean-agent/lean-bench 真正证明 ```sh lean-bench datasets/goodman-1.6.jsonl --output results/goodman-1.6-001 \ --lean-project /path/to/your/mathlib-project --lean-command '["lake","env","lean"]' \ --model ... --base-url ... ``` ### 6. 把证出来的定理组装成一份可复用的库文件 ```sh python3 textbook/build_library.py datasets/goodman-1.6.jsonl \ results/goodman-1.6-001/results.jsonl --out lib/Chapter01Section06.lean ``` 只有这次跑真的证出来的定理（`results.jsonl` 里 `success: true`）才会被收进 去，直接复用验证时确认过的那个证明，不会引入新的证明风险。后续章节要用这些 已证定理时，`import` 这份文件——注意这只是把已证结果攒成一个文件，不是一个真 正的 Lake 包/模块边界。 ## 本机环境准备：一个带 Mathlib 的 Lake 项目 Cowork 这边的沙盒没有 Lean，`check_statements.py` 和真正跑 `lean-agent`/ `lean-bench` 都需要在你本机（或者别的有 Lean 的环境）完成。如果还没有这样一 个项目： ```sh cd ~/ProjectResearch # 随便一个地方 lake +leanprover/lean4:v4.33.1 new mathlib-bench math cd mathlib-bench lake exe cache get # 下载 Mathlib 预编译缓存，比从源码编译快得多 lake build ``` 之后 `--lean-project` 就指到 `mathlib-bench` 这个目录，`--lean-command` 用 `'["lake","env","lean"]'`。 ## 反馈循环 我（claude-bot）在 ProjectResearch 里生成/修改数据集和代码 → 提交并 push 到 `Zayden-Jung/lean-bench`（用 claude-bot 的 token） → 你在本机 `git pull` → 跑 `check_statements.py` / `lean-bench` → 把失败的条目 id 和 Lean 报的错发 给我 → 我改完再 push。不需要额外工具，就是正常的 git 往返。