From 5aa048593c29855f7208e868aeb3363015bd8e34 Mon Sep 17 00:00:00 2001 From: Claude Bot Date: Fri, 18 Sep 2026 17:03:07 +0000 Subject: [PATCH] Note goodman-1.6 dataset now fully elaborates (test push) Co-Authored-By: Claude Sonnet 5 Claude-Session: https://claude.ai/code/session_017vbLFFJiHSZqGZHEkjvG5x --- README.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/README.md b/README.md index e94a251..e55cb85 100644 --- a/README.md +++ b/README.md @@ -32,3 +32,8 @@ mock 返回固定证明，仍由真实 Lean 检查。真实 LLM 需配置 endpoi `textbook/` 下有一套从教材 PDF 生成 lean-bench 数据集的工具（LLM 辅助抽取 Theorem/Proposition/Lemma/Corollary，配 Definition 清单，事后把证出来的结果 组装成可复用的 Lean 库文件），用法见 [textbook/README.md](textbook/README.md)。 + +## 状态数据集进度（更新于 2026-09-18） + +goodman-1.6.jsonl 全部 21 条 statement 已通过本地 Lean elaboration 检查 +（`check_statements.py`），定义清单中的幻觉 Mathlib 引用也已修正。