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

---
 leanbench/README.md | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

diff --git a/leanbench/README.md b/leanbench/README.md
index 1184343..1381b39 100644
--- a/leanbench/README.md
+++ b/leanbench/README.md
@@ -1,10 +1,10 @@
-[__init__.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/__init__.py)
+[__init__.py](lean-bench/leanbench/__init__.py)
 包入口和项目简介：
 - 定义 __version__ = "0.2.0"。
 - 用模块文档说明四阶段流水线。
 - 不包含实际业务逻辑。
 
-[config.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/config.py)
+[config.py](lean-bench/leanbench/config.py)
 集中管理运行配置：
 - 读取 .env，且不会让空环境变量遮蔽 .env 中的有效值。
 - 定义 LLMSettings。
@@ -15,7 +15,7 @@
 - 支持 JSON 数组形式的 Lean 命令。
 这是 CLI、pipeline、OCR 和 Lean 验证之间的配置枢纽。
 
-[llm.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/llm.py)
+[llm.py](lean-bench/leanbench/llm.py)
 OpenAI-compatible LLM 客户端：
 - 使用标准库 urllib，不依赖 OpenAI SDK。
 - 调用 /chat/completions。
@@ -27,7 +27,7 @@ OpenAI-compatible LLM 客户端：
 - 提供 ScriptedClient，让测试可以用固定回复代替真实网络。
 它既服务于片段检测，也服务于视觉 OCR 和 Lean 生成。
 
-[document.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/document.py)
+[document.py](lean-bench/leanbench/document.py)
 文档抽象和页面读取：
 - 读取 PDF。
 - 支持 form-feed 分页的 .txt 文件。
@@ -42,7 +42,7 @@ OpenAI-compatible LLM 客户端：
 - 用 PageWindow 在“全局窗口偏移”和“页内偏移”之间转换。
 这里决定后续系统实际看到的页面文本是什么。
 
-[ocr.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/ocr.py)
+[ocr.py](lean-bench/leanbench/ocr.py)
 OCR 与文本质量判断：
 - 把 PDF 页面渲染为 PNG。
 - VisionLLMBackend：把页面图片发给视觉模型。
@@ -54,7 +54,7 @@ OCR 与文本质量判断：
 - 去掉模型偶尔返回的 markdown fence。
 其文本质量规则明显针对 Iowa 代数教材做过专门校准。
 
-[anchors.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/anchors.py)
+[anchors.py](lean-bench/leanbench/anchors.py)
 锚点解析：
 - 模型不直接计算字符下标，而是返回首尾引用。
 - 首先尝试精确匹配。
@@ -65,7 +65,7 @@ OCR 与文本质量判断：
 - 无法可靠匹配时返回 unresolved，不随意猜测。
 这是保证检测结果能映射回原书位置的关键层。
 
-[detect.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/detect.py)
+[detect.py](lean-bench/leanbench/detect.py)
 数学内容检测：
 - 定义 statement 和 problem 两种类型。
 - 构造检测用系统提示词。
@@ -79,7 +79,7 @@ OCR 与文本质量判断：
 - 可以把检测结果写成 JSONL。
 这里负责“书中哪些内容值得形式化”。
 
-[formalize.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/formalize.py)
+[formalize.py](lean-bench/leanbench/formalize.py)
 Lean 代码生成：
 - 把一个 Detection 转换为一个 Lean 顶层声明。
 - 定义生成 Lean 的系统提示词。
@@ -94,7 +94,7 @@ Lean 代码生成：
 - 单条失败不会中断整批。
 它是目前实际效果最弱、也最值得投入改进的模块。
 
-[verify.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/verify.py)
+[verify.py](lean-bench/leanbench/verify.py)
 Lean 验证器：
 - 生成临时 .lean 文件。
 - 添加 import Mathlib 和模型要求的 imports。
@@ -109,7 +109,7 @@ Lean 验证器：
 - NullChecker 用于未安装 Lean 或主动跳过验证的场景。
 它每个条目启动一次 Lean 进程，整书运行时成本很高。
 
-[typeindex.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/typeindex.py)
+[typeindex.py](lean-bench/leanbench/typeindex.py)
 Lean 类型索引：
 - 用正则识别 theorem、lemma、def、structure 等声明。
 - 提取 binder 中的输入类型。
@@ -120,7 +120,7 @@ Lean 类型索引：
 - 为类型标记 input、goal 或 own 角色。
 这是启发式解析，不是 Lean AST 解析，因此复杂语法下可能漏检或误判。
 
-[db.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/db.py)
+[db.py](lean-bench/leanbench/db.py)
 SQLite 数据库：
 - 创建 meta、sources、items、item_types 表。
 - 建立来源、页码、kind、verified 和类型索引。
@@ -135,7 +135,7 @@ SQLite 数据库：
 - 默认导出时排除大块源码和诊断。
 数据库设计比较直接，但整次 ingest 没有总事务保护。
 
-[pipeline.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/pipeline.py)
+[pipeline.py](lean-bench/leanbench/pipeline.py)
 把所有阶段串起来：
 1. 加载配置。
 2. 构造 LLM 客户端。
@@ -149,7 +149,7 @@ SQLite 数据库：
 IngestResult.summary() 会统计检测、形式化、验证、证明和写入数量。
 主要风险是第 5 步发生得太早：后续失败时旧数据已经被删除。
 
-[cli.py](/Users/zzyang/ProjectResearch/lean-bench/leanbench/cli.py)
+[cli.py](lean-bench/leanbench/cli.py)
 命令行界面：
 - doctor：检查 PDF、Lean 和 LLM。
 - ingest：执行完整流水线。