claude-bot
caedf2e6f4
- extract_section.py: slice a book section out of a pdftotext -layout dump and list its labeled Theorem/Proposition/Lemma/Corollary/Definition items. - formalize.py: LLM-formalize a section into Lean 4 candidate statements (preferring Mathlib vocabulary) plus a definitions manifest. - check_statements.py: elaboration-only sanity check against a real Mathlib-backed Lean project (must run outside the Cowork sandbox, which has no Lean toolchain and can't run macOS binaries anyway). - build_library.py: assemble solved lean-bench results into a reusable .lean file, reusing each winning proof verbatim. - llm.py: standalone OpenAI-compatible chat client + .env loader, kept independent of lean_agent so this pipeline works without it installed. - Source PDFs and raw/layout text dumps are gitignored (copyrighted material); only code and the final short Lean statement datasets are tracked.
134 lines
6.4 KiB
Markdown
134 lines
6.4 KiB
Markdown
# 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 往返。
|