From a030939d75e9eb323b9f80e08e9d5cc37a7486a2 Mon Sep 17 00:00:00 2001
From: Zayden-Jung <zayden.jung@entroia.com>
Date: Tue, 22 Sep 2026 15:07:49 +0000
Subject: [PATCH] Add leanbench/README.md

---
 leanbench/README.md | 168 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 168 insertions(+)
 create mode 100644 leanbench/README.md

diff --git a/leanbench/README.md b/leanbench/README.md
new file mode 100644
index 0000000..1184343
--- /dev/null
+++ b/leanbench/README.md
@@ -0,0 +1,168 @@
+[__init__.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/__init__.py)
+包入口和项目简介：
+- 定义 __version__ = "0.2.0"。
+- 用模块文档说明四阶段流水线。
+- 不包含实际业务逻辑。
+
+[config.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/config.py)
+集中管理运行配置：
+- 读取 .env，且不会让空环境变量遮蔽 .env 中的有效值。
+- 定义 LLMSettings。
+- 定义 LeanSettings。
+- 定义 OcrSettings。
+- 定义总的 Settings。
+- 对错误整数、浮点配置使用默认值。
+- 支持 JSON 数组形式的 Lean 命令。
+这是 CLI、pipeline、OCR 和 Lean 验证之间的配置枢纽。
+
+[llm.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/llm.py)
+OpenAI-compatible LLM 客户端：
+- 使用标准库 urllib，不依赖 OpenAI SDK。
+- 调用 /chat/completions。
+- 支持不同 endpoint 和模型。
+- 从指定环境变量读取 API Key。
+- 实现超时、重试和错误包装。
+- 从 markdown fence 或夹杂说明的回复中提取 JSON。
+- 从模型回复中提取 Lean 代码块。
+- 提供 ScriptedClient，让测试可以用固定回复代替真实网络。
+它既服务于片段检测，也服务于视觉 OCR 和 Lean 生成。
+
+[document.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/document.py)
+文档抽象和页面读取：
+- 读取 PDF。
+- 支持 form-feed 分页的 .txt 文件。
+- 给每页分配从 1 开始的页码。
+- 计算源文件 SHA-256 和页面 checksum。
+- 规范化文本。
+- 按页范围加载。
+- 在 text、auto、ocr 三种模式间选择。
+- OCR 失败时保留嵌入文本。
+- 如果要求整批 OCR，但所有页面都失败，则明确报错。
+- 提供跨页文本切片。
+- 用 PageWindow 在“全局窗口偏移”和“页内偏移”之间转换。
+这里决定后续系统实际看到的页面文本是什么。
+
+[ocr.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/ocr.py)
+OCR 与文本质量判断：
+- 把 PDF 页面渲染为 PNG。
+- VisionLLMBackend：把页面图片发给视觉模型。
+- TesseractBackend：调用本地 Tesseract。
+- 用特殊乱码字符和 D/C/W 操作符模式判断嵌入文本是否损坏。
+- 实现 OCR 磁盘缓存。
+- 缓存键包含文档哈希、页码、DPI 和 OCR 后端。
+- 记录各页 OCR 失败原因。
+- 去掉模型偶尔返回的 markdown fence。
+其文本质量规则明显针对 Iowa 代数教材做过专门校准。
+
+[anchors.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/anchors.py)
+锚点解析：
+- 模型不直接计算字符下标，而是返回首尾引用。
+- 首先尝试精确匹配。
+- 然后尝试忽略空白差异的匹配。
+- 最后尝试模糊匹配。
+- 将首尾引用组合成完整 span。
+- 记录匹配方法和分数。
+- 无法可靠匹配时返回 unresolved，不随意猜测。
+这是保证检测结果能映射回原书位置的关键层。
+
+[detect.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/detect.py)
+数学内容检测：
+- 定义 statement 和 problem 两种类型。
+- 构造检测用系统提示词。
+- 要求模型返回 JSON 和首尾原文引用。
+- 清洗模型返回的 kind、label、summary。
+- 调用锚点解析得到精确页码和字符范围。
+- 发现条目延续到下一页时扩大窗口重新检测。
+- 达到窗口上限后用 truncated 标记。
+- 一个页面失败时继续处理其他页面。
+- 对相同起点的重复结果去重。
+- 可以把检测结果写成 JSONL。
+这里负责“书中哪些内容值得形式化”。
+
+[formalize.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/formalize.py)
+Lean 代码生成：
+- 把一个 Detection 转换为一个 Lean 顶层声明。
+- 定义生成 Lean 的系统提示词。
+- 区分书中已有结论和留给读者的问题。
+- 对 problem 只生成带 sorry 的待证明命题。
+- 清洗模型返回的 imports、代码、名称和置信度。
+- 删除代码正文中多余的 import。
+- 调用 Lean checker。
+- 将 Lean 编译诊断发回模型进行修复。
+- 控制最大修复次数。
+- 为结果计算类型索引。
+- 单条失败不会中断整批。
+它是目前实际效果最弱、也最值得投入改进的模块。
+
+[verify.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/verify.py)
+Lean 验证器：
+- 生成临时 .lean 文件。
+- 添加 import Mathlib 和模型要求的 imports。
+- 调用配置的 lake env lean。
+- 设置超时。
+- 收集 stdout 和 stderr。
+- 判断 Lean 是否接受声明。
+- 检查声明是否使用 sorry。
+- 定义：
+  - verified：Lean 接受。
+  - proved：Lean 接受、完整模式、没有 sorry。
+- NullChecker 用于未安装 Lean 或主动跳过验证的场景。
+它每个条目启动一次 Lean 进程，整书运行时成本很高。
+
+[typeindex.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/typeindex.py)
+Lean 类型索引：
+- 用正则识别 theorem、lemma、def、structure 等声明。
+- 提取 binder 中的输入类型。
+- 对定理提取 goal 类型。
+- 对定义提取其自身类型。
+- 把 ℕ、ℤ、ℚ、ℝ 等标准化成 Lean 名称。
+- 将模型提供的补充类型与自动提取结果合并。
+- 为类型标记 input、goal 或 own 角色。
+这是启发式解析，不是 Lean AST 解析，因此复杂语法下可能漏检或误判。
+
+[db.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/db.py)
+SQLite 数据库：
+- 创建 meta、sources、items、item_types 表。
+- 建立来源、页码、kind、verified 和类型索引。
+- 在 SQLite 支持时启用 FTS5。
+- 用“源文件哈希 + span”生成稳定 item ID。
+- 插入或更新来源和条目。
+- 更新条目时删除旧类型，避免残留。
+- 按来源或起始页范围删除数据。
+- 支持按类型、角色、kind、来源、页码、文本、验证状态查询。
+- 提供来源统计和类型频率。
+- 导出 JSONL。
+- 默认导出时排除大块源码和诊断。
+数据库设计比较直接，但整次 ingest 没有总事务保护。
+
+[pipeline.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/pipeline.py)
+把所有阶段串起来：
+1. 加载配置。
+2. 构造 LLM 客户端。
+3. 构造 OCR reader。
+4. 加载文档。
+5. 删除旧页段结果。
+6. 检测数学片段。
+7. 生成并验证 Lean。
+8. 写入数据库。
+9. 生成运行摘要。
+IngestResult.summary() 会统计检测、形式化、验证、证明和写入数量。
+主要风险是第 5 步发生得太早：后续失败时旧数据已经被删除。
+
+[cli.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/cli.py)
+命令行界面：
+- doctor：检查 PDF、Lean 和 LLM。
+- ingest：执行完整流水线。
+- detect：只做数学内容检测。
+- extract：查看嵌入文本或 OCR 文本。
+- search：查询数据库。
+- sources：列出来源。
+- stats：输出统计和高频类型。
+- export：导出 JSONL。
+- drop：删除来源或指定页段。
+同时负责：
+- 解析 30-45 一类页码范围。
+- 将命令行 OCR 参数覆盖到 Settings。
+- 将常见异常转换成退出码。
+- 注册 lean-bench 命令的 main()。
+目前没有独立的 CLI 测试文件。
\ No newline at end of file