lean-bench/leanbench

__init__.py 包入口和项目简介：

• 定义 version = "0.2.0"。
• 用模块文档说明四阶段流水线。
• 不包含实际业务逻辑。

config.py 集中管理运行配置：

• 读取 .env，且不会让空环境变量遮蔽 .env 中的有效值。
• 定义 LLMSettings。
• 定义 LeanSettings。
• 定义 OcrSettings。
• 定义总的 Settings。
• 对错误整数、浮点配置使用默认值。
• 支持 JSON 数组形式的 Lean 命令。 这是 CLI、pipeline、OCR 和 Lean 验证之间的配置枢纽。

llm.py OpenAI-compatible LLM 客户端：

• 使用标准库 urllib，不依赖 OpenAI SDK。
• 调用 /chat/completions。
• 支持不同 endpoint 和模型。
• 从指定环境变量读取 API Key。
• 实现超时、重试和错误包装。
• 从 markdown fence 或夹杂说明的回复中提取 JSON。
• 从模型回复中提取 Lean 代码块。
• 提供 ScriptedClient，让测试可以用固定回复代替真实网络。 它既服务于片段检测，也服务于视觉 OCR 和 Lean 生成。

document.py 文档抽象和页面读取：

• 读取 PDF。
• 支持 form-feed 分页的 .txt 文件。
• 给每页分配从 1 开始的页码。
• 计算源文件 SHA-256 和页面 checksum。
• 规范化文本。
• 按页范围加载。
• 在 text、auto、ocr 三种模式间选择。
• OCR 失败时保留嵌入文本。
• 如果要求整批 OCR，但所有页面都失败，则明确报错。
• 提供跨页文本切片。
• 用 PageWindow 在“全局窗口偏移”和“页内偏移”之间转换。 这里决定后续系统实际看到的页面文本是什么。

ocr.py OCR 与文本质量判断：

• 把 PDF 页面渲染为 PNG。
• VisionLLMBackend：把页面图片发给视觉模型。
• TesseractBackend：调用本地 Tesseract。
• 用特殊乱码字符和 D/C/W 操作符模式判断嵌入文本是否损坏。
• 实现 OCR 磁盘缓存。
• 缓存键包含文档哈希、页码、DPI 和 OCR 后端。
• 记录各页 OCR 失败原因。
• 去掉模型偶尔返回的 markdown fence。 其文本质量规则明显针对 Iowa 代数教材做过专门校准。

anchors.py 锚点解析：

• 模型不直接计算字符下标，而是返回首尾引用。
• 首先尝试精确匹配。
• 然后尝试忽略空白差异的匹配。
• 最后尝试模糊匹配。
• 将首尾引用组合成完整 span。
• 记录匹配方法和分数。
• 无法可靠匹配时返回 unresolved，不随意猜测。 这是保证检测结果能映射回原书位置的关键层。

detect.py 数学内容检测：

• 定义 statement 和 problem 两种类型。
• 构造检测用系统提示词。
• 要求模型返回 JSON 和首尾原文引用。
• 清洗模型返回的 kind、label、summary。
• 调用锚点解析得到精确页码和字符范围。
• 发现条目延续到下一页时扩大窗口重新检测。
• 达到窗口上限后用 truncated 标记。
• 一个页面失败时继续处理其他页面。
• 对相同起点的重复结果去重。
• 可以把检测结果写成 JSONL。 这里负责“书中哪些内容值得形式化”。

formalize.py Lean 代码生成：

• 把一个 Detection 转换为一个 Lean 顶层声明。
• 定义生成 Lean 的系统提示词。
• 区分书中已有结论和留给读者的问题。
• 对 problem 只生成带 sorry 的待证明命题。
• 清洗模型返回的 imports、代码、名称和置信度。
• 删除代码正文中多余的 import。
• 调用 Lean checker。
• 将 Lean 编译诊断发回模型进行修复。
• 控制最大修复次数。
• 为结果计算类型索引。
• 单条失败不会中断整批。 它是目前实际效果最弱、也最值得投入改进的模块。

verify.py Lean 验证器：

• 生成临时 .lean 文件。
• 添加 import Mathlib 和模型要求的 imports。
• 调用配置的 lake env lean。
• 设置超时。
• 收集 stdout 和 stderr。
• 判断 Lean 是否接受声明。
• 检查声明是否使用 sorry。
• 定义：
  • verified：Lean 接受。
  • proved：Lean 接受、完整模式、没有 sorry。
• NullChecker 用于未安装 Lean 或主动跳过验证的场景。 它每个条目启动一次 Lean 进程，整书运行时成本很高。

typeindex.py Lean 类型索引：

• 用正则识别 theorem、lemma、def、structure 等声明。
• 提取 binder 中的输入类型。
• 对定理提取 goal 类型。
• 对定义提取其自身类型。
• 把 ℕ、ℤ、ℚ、ℝ 等标准化成 Lean 名称。
• 将模型提供的补充类型与自动提取结果合并。
• 为类型标记 input、goal 或 own 角色。 这是启发式解析，不是 Lean AST 解析，因此复杂语法下可能漏检或误判。

db.py SQLite 数据库：

• 创建 meta、sources、items、item_types 表。
• 建立来源、页码、kind、verified 和类型索引。
• 在 SQLite 支持时启用 FTS5。
• 用“源文件哈希 + span”生成稳定 item ID。
• 插入或更新来源和条目。
• 更新条目时删除旧类型，避免残留。
• 按来源或起始页范围删除数据。
• 支持按类型、角色、kind、来源、页码、文本、验证状态查询。
• 提供来源统计和类型频率。
• 导出 JSONL。
• 默认导出时排除大块源码和诊断。 数据库设计比较直接，但整次 ingest 没有总事务保护。

pipeline.py 把所有阶段串起来：

1. 加载配置。
2. 构造 LLM 客户端。
3. 构造 OCR reader。
4. 加载文档。
5. 删除旧页段结果。
6. 检测数学片段。
7. 生成并验证 Lean。
8. 写入数据库。
9. 生成运行摘要。 IngestResult.summary() 会统计检测、形式化、验证、证明和写入数量。 主要风险是第 5 步发生得太早：后续失败时旧数据已经被删除。

cli.py 命令行界面：

• doctor：检查 PDF、Lean 和 LLM。
• ingest：执行完整流水线。
• detect：只做数学内容检测。
• extract：查看嵌入文本或 OCR 文本。
• search：查询数据库。
• sources：列出来源。
• stats：输出统计和高频类型。
• export：导出 JSONL。
• drop：删除来源或指定页段。 同时负责：
• 解析 30-45 一类页码范围。
• 将命令行 OCR 参数覆盖到 Settings。
• 将常见异常转换成退出码。
• 注册 lean-bench 命令的 main()。 目前没有独立的 CLI 测试文件。