From caedf2e6f461125cf569788b04ee22ded6897468 Mon Sep 17 00:00:00 2001 From: Claude Bot Date: Thu, 17 Sep 2026 17:04:19 +0000 Subject: [PATCH] Add textbook formalization pipeline (extract -> LLM formalize -> elaboration check -> library assembly) - 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. --- .gitignore | 6 ++ README.md | 6 ++ tests/test_build_library.py | 61 ++++++++++++ tests/test_extract_section.py | 49 ++++++++++ tests/test_formalize.py | 58 +++++++++++ textbook/README.md | 133 +++++++++++++++++++++++++ textbook/__init__.py | 0 textbook/build_library.py | 82 ++++++++++++++++ textbook/check_statements.py | 75 +++++++++++++++ textbook/extract_section.py | 73 ++++++++++++++ textbook/formalize.py | 165 ++++++++++++++++++++++++++++++++ textbook/llm.py | 46 +++++++++ textbook/section_1_6.index.json | 117 ++++++++++++++++++++++ 13 files changed, 871 insertions(+) create mode 100644 tests/test_build_library.py create mode 100644 tests/test_extract_section.py create mode 100644 tests/test_formalize.py create mode 100644 textbook/README.md create mode 100644 textbook/__init__.py create mode 100644 textbook/build_library.py create mode 100644 textbook/check_statements.py create mode 100644 textbook/extract_section.py create mode 100644 textbook/formalize.py create mode 100644 textbook/llm.py create mode 100644 textbook/section_1_6.index.json diff --git a/.gitignore b/.gitignore index 2c255f8..03a9c1c 100644 --- a/.gitignore +++ b/.gitignore @@ -3,3 +3,9 @@ __pycache__/ .venv/ .env results/ + +# Source textbook and raw/derived full-text dumps: copyrighted material, never commit. +# Only code and the final short Lean statement datasets under datasets/ are tracked. +*.pdf +textbook/*.txt +textbook/*_raw.txt diff --git a/README.md b/README.md index d91479f..e94a251 100644 --- a/README.md +++ b/README.md @@ -26,3 +26,9 @@ python3 -m unittest discover -s tests -v ``` mock 返回固定证明，仍由真实 Lean 检查。真实 LLM 需配置 endpoint/model 或适配器。 + +## 教科书形式化流水线 + +`textbook/` 下有一套从教材 PDF 生成 lean-bench 数据集的工具（LLM 辅助抽取 +Theorem/Proposition/Lemma/Corollary，配 Definition 清单，事后把证出来的结果 +组装成可复用的 Lean 库文件），用法见 [textbook/README.md](textbook/README.md)。 diff --git a/tests/test_build_library.py b/tests/test_build_library.py new file mode 100644 index 0000000..4a4e960 --- /dev/null +++ b/tests/test_build_library.py @@ -0,0 +1,61 @@ +import json +import tempfile +import unittest +from pathlib import Path + +from textbook.build_library import build + + +def write_jsonl(path, records): + path.write_text('\n'.join(json.dumps(r) for r in records) + '\n', encoding='utf-8') + + +class BuildLibraryTests(unittest.TestCase): + def test_build_includes_only_solved_theorems_and_hoists_shared_imports(self): + with tempfile.TemporaryDirectory() as directory: + directory = Path(directory) + dataset = directory / 'dataset.jsonl' + results = directory / 'results.jsonl' + write_jsonl(dataset, [ + {"id": "solved-one", "statement": "True", "prelude": "import Mathlib", + "source_label": "Theorem 1", "natural_language": "trivial"}, + {"id": "unsolved-one", "statement": "False", "prelude": "import Mathlib", + "source_label": "Theorem 2", "natural_language": "not actually true"}, + ]) + write_jsonl(results, [ + {"id": "solved-one", "success": True, + "attempts": [{"proof": "trivial", "success": True, "diagnostics": ""}]}, + {"id": "unsolved-one", "success": False, "attempts": []}, + ]) + + text, solved, skipped = build(dataset, results) + + self.assertEqual(solved, ['solved-one']) + self.assertEqual(skipped, ['unsolved-one']) + self.assertIn('import Mathlib', text) + self.assertEqual(text.count('import Mathlib'), 1) # hoisted once, not per-theorem + self.assertIn('theorem solved_one : True := by', text) + self.assertNotIn('unsolved_one', text) + + def test_build_keeps_non_import_prelude_attached_per_theorem(self): + with tempfile.TemporaryDirectory() as directory: + directory = Path(directory) + dataset = directory / 'dataset.jsonl' + results = directory / 'results.jsonl' + write_jsonl(dataset, [ + {"id": "custom-def", "statement": "myPred 1", "prelude": "def myPred (n : Nat) := True", + "source_label": "Theorem 3", "natural_language": ""}, + ]) + write_jsonl(results, [ + {"id": "custom-def", "success": True, + "attempts": [{"proof": "trivial", "success": True, "diagnostics": ""}]}, + ]) + + text, solved, skipped = build(dataset, results) + + self.assertIn('def myPred (n : Nat) := True', text) + self.assertEqual(solved, ['custom-def']) + + +if __name__ == '__main__': + unittest.main() diff --git a/tests/test_extract_section.py b/tests/test_extract_section.py new file mode 100644 index 0000000..fc62248 --- /dev/null +++ b/tests/test_extract_section.py @@ -0,0 +1,49 @@ +import unittest +from textbook.extract_section import extract_section, labeled_statements + +FIXTURE = """\ +1.6. Divisibility in the Integers +intro text + +Proposition 1.6.1. +body + +Theorem 1.6.6. There are infinitely many prime numbers. +Proof. blah +36 1. ALGEBRAIC THEMES + + +Theorem 1.6.6. There are infinitely many prime numbers. +Proof continues after a page break, repeats the label. + +1.7. Modular Arithmetic +next section text +""" + + +class ExtractSectionTests(unittest.TestCase): + def test_extract_section_slices_between_headings(self): + section = extract_section(FIXTURE, '1.6. Divisibility in the Integers', '1.7. Modular Arithmetic') + self.assertIn('Theorem 1.6.6', section) + self.assertNotIn('next section text', section) + + def test_extract_section_missing_heading_raises(self): + with self.assertRaises(ValueError): + extract_section(FIXTURE, '1.6. Divisibility in the Integers', '9.9. Does Not Exist') + + def test_labeled_statements_dedupes_and_orders(self): + section = extract_section(FIXTURE, '1.6. Divisibility in the Integers', '1.7. Modular Arithmetic') + items = labeled_statements(section, '1.6.') + labels = [item['label'] for item in items] + # Theorem 1.6.6 appears twice (page-break repeat) but must be kept once, and + # book order (1.6.1 before 1.6.6) must be preserved. + self.assertEqual(labels, ['1.6.1', '1.6.6']) + + def test_labeled_statements_filters_by_prefix(self): + section = extract_section(FIXTURE, '1.6. Divisibility in the Integers', '1.7. Modular Arithmetic') + items = labeled_statements(section, '1.7.') + self.assertEqual(items, []) + + +if __name__ == '__main__': + unittest.main() diff --git a/tests/test_formalize.py b/tests/test_formalize.py new file mode 100644 index 0000000..fbf33cf --- /dev/null +++ b/tests/test_formalize.py @@ -0,0 +1,58 @@ +import json +import unittest + +from textbook.formalize import extract_json_block, validate + +VALID_REPLY = """Here is the result: +```json +{ + "definitions": [ + {"label": "Definition 1.6.3", "concept": "prime number", "mathlib_ref": "Nat.Prime", + "lean_code": null, "notes": ""} + ], + "theorems": [ + {"id": "goodman-1-6-6", "source_label": "Theorem 1.6.6", "kind": "theorem", + "statement": "\\u2200 n : \\u2115, \\u2203 p, p > n \\u2227 p.Prime", + "prelude": "import Mathlib", "natural_language": "There are infinitely many primes.", + "requires": ["Nat.Prime"], "include_in_bench": true, "exclude_reason": null} + ] +} +``` +""" + + +class FormalizeParsingTests(unittest.TestCase): + def test_extract_json_block_from_fenced_reply(self): + data = extract_json_block(VALID_REPLY) + self.assertEqual(set(data), {"definitions", "theorems"}) + + def test_extract_json_block_without_fence_falls_back_to_whole_text(self): + payload = '{"theorems": [], "definitions": []}' + self.assertEqual(extract_json_block(payload), json.loads(payload)) + + def test_validate_accepts_well_formed_response(self): + data = extract_json_block(VALID_REPLY) + theorems, definitions = validate(data) + self.assertEqual(len(theorems), 1) + self.assertEqual(len(definitions), 1) + + def test_validate_rejects_missing_field(self): + data = {"theorems": [{"id": "x", "source_label": "Theorem 1", "statement": "True"}], + "definitions": []} + with self.assertRaises(ValueError): + validate(data) + + def test_validate_rejects_duplicate_ids(self): + entry = {"id": "dup", "source_label": "Theorem 1", "kind": "theorem", "statement": "True", + "prelude": "import Mathlib", "include_in_bench": True} + data = {"theorems": [entry, dict(entry)], "definitions": []} + with self.assertRaises(ValueError): + validate(data) + + def test_validate_rejects_non_object_response(self): + with self.assertRaises(ValueError): + validate([]) + + +if __name__ == '__main__': + unittest.main() diff --git a/textbook/README.md b/textbook/README.md new file mode 100644 index 0000000..76fd32e --- /dev/null +++ b/textbook/README.md @@ -0,0 +1,133 @@ +# 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 往返。 diff --git a/textbook/__init__.py b/textbook/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/textbook/build_library.py b/textbook/build_library.py new file mode 100644 index 0000000..fc9f07d --- /dev/null +++ b/textbook/build_library.py @@ -0,0 +1,82 @@ +"""Assemble a reusable Lean library file from a completed lean-bench run. + +Only theorems that actually solved (results.jsonl success == true) go in; each one's +exact winning proof (its last, successful attempt) is reused verbatim, re-wrapped in the +same `theorem : := by ...` shape lean-bench's verifier already checked, +so the assembled file carries no new proof risk beyond what that run already confirmed -- +this script does not itself call Lean. + +Plain `import ...` preludes are deduplicated and hoisted to the top of the file; any +other prelude content (a local definition, say) is kept attached to its own theorem +instead of being collapsed, since it isn't necessarily shared with the rest. + +A library assembled this way is only as trustworthy as the run it came from: rerun +check_statements.py / lean-bench yourself before importing it into something else you +care about, and treat --module-name as documentation, not a real Lean module boundary +(this script emits one flat .lean file, not a package). +""" +import argparse +import json +from pathlib import Path + + +def load_jsonl(path): + return [json.loads(line) for line in path.read_text(encoding='utf-8').splitlines() if line.strip()] + + +def build(dataset_path, results_path): + dataset = {t['id']: t for t in load_jsonl(dataset_path)} + results = {r['id']: r for r in load_jsonl(results_path)} + + shared_imports = set() + per_theorem_prelude = {} + for task_id, task in dataset.items(): + prelude = task.get('prelude', '').strip() + if not prelude: + continue + if all(line.strip().startswith('import ') for line in prelude.splitlines()): + shared_imports.update(line.strip() for line in prelude.splitlines()) + else: + per_theorem_prelude[task_id] = prelude + + lines = ['-- Generated by textbook/build_library.py -- do not hand-edit proofs;', + '-- regenerate from a fresh lean-bench run instead.', ''] + lines.extend(sorted(shared_imports)) + lines.append('') + + solved, skipped = [], [] + for task_id, task in dataset.items(): + result = results.get(task_id) + if not result or not result.get('success') or not result.get('attempts'): + skipped.append(task_id) + continue + proof = result['attempts'][-1]['proof'] + comment = f'-- {task.get("source_label", task_id)}: {task.get("natural_language", "")}'.rstrip() + lines.append(comment) + if task_id in per_theorem_prelude: + lines.append(per_theorem_prelude[task_id]) + lean_name = task_id.replace('-', '_') + lines.append(f'theorem {lean_name} : {task["statement"]} := by') + lines.extend(' ' + line for line in proof.splitlines()) + lines.append('') + solved.append(task_id) + + return '\n'.join(lines), solved, skipped + + +def main(): + parser = argparse.ArgumentParser(description='Assemble a Lean library file from a solved lean-bench dataset') + parser.add_argument('dataset', type=Path) + parser.add_argument('results', type=Path, help="a lean-bench run's results.jsonl") + parser.add_argument('--out', type=Path, required=True) + args = parser.parse_args() + + text, solved, skipped = build(args.dataset, args.results) + args.out.write_text(text + '\n', encoding='utf-8') + print(f'{len(solved)} theorems assembled -> {args.out}') + if skipped: + print(f'{len(skipped)} skipped (not solved in this run): {", ".join(skipped)}') + + +if __name__ == '__main__': + main() diff --git a/textbook/check_statements.py b/textbook/check_statements.py new file mode 100644 index 0000000..52c7fa3 --- /dev/null +++ b/textbook/check_statements.py @@ -0,0 +1,75 @@ +"""Elaboration-only sanity check for candidate Lean statements from formalize.py. + +Checks whether `theorem _ : statement := by sorry` type-checks under the task's +prelude -- i.e. whether the statement is well-formed Lean using identifiers that +actually exist. This does NOT verify the statement is provable, or even that it +faithfully represents the book (that's still on you to spot-check); it only catches +hallucinated Mathlib names and syntax errors for free, before spending any lean-agent +proof attempts on them. + +Must run on a machine with `lean`/`lake` installed and, for anything using Mathlib +(almost everything here), a Lake project that already has Mathlib built -- point +--lean-project at it and pass --lean-command '["lake","env","lean"]'. This script +cannot run inside a Cowork sandbox: see lean-bench/textbook/README.md. +""" +import argparse +import json +import subprocess +import tempfile +from dataclasses import dataclass +from pathlib import Path + + +@dataclass +class ElabResult: + ok: bool + diagnostics: str + + +def elaborates(prelude, statement, command=None, cwd=None, timeout=30): + command = command or ['lean'] + source = (prelude + '\n' if prelude else '') + 'theorem lean_bench_sanity_check : ' + statement + ' := by sorry\n' + with tempfile.TemporaryDirectory(prefix='lean-sanity-', dir=cwd) as directory: + path = Path(directory) / 'SanityCheck.lean' + path.write_text(source, encoding='utf-8') + try: + result = subprocess.run([*command, str(path)], cwd=cwd, capture_output=True, + text=True, timeout=timeout) + except subprocess.TimeoutExpired: + return ElabResult(False, 'Lean timeout') + diagnostics = result.stdout + result.stderr + ok = result.returncode == 0 and 'error:' not in diagnostics + return ElabResult(ok, diagnostics[-8000:]) + + +def main(): + parser = argparse.ArgumentParser(description='Check that candidate statements elaborate (not that they are provable)') + parser.add_argument('dataset', type=Path, help='JSONL with id, statement, optional prelude') + parser.add_argument('--lean-command', default='["lean"]', help='JSON argv array; e.g. ["lake","env","lean"]') + parser.add_argument('--lean-project', help='Lean/Lake project working directory (needs Mathlib built)') + parser.add_argument('--timeout', type=float, default=60) + parser.add_argument('--report', type=Path, help='Write JSONL of {id, ok, diagnostics} here') + args = parser.parse_args() + + command = json.loads(args.lean_command) + tasks = [json.loads(line) for line in args.dataset.read_text(encoding='utf-8').splitlines() if line.strip()] + reports = [] + failed = 0 + for task in tasks: + result = elaborates(task.get('prelude', ''), task['statement'], command, args.lean_project, args.timeout) + reports.append({"id": task['id'], "ok": result.ok, "diagnostics": result.diagnostics}) + print(('OK ' if result.ok else 'FAIL') + ' ' + task['id']) + if not result.ok: + failed += 1 + + if args.report: + with args.report.open('w', encoding='utf-8') as stream: + for r in reports: + stream.write(json.dumps(r, ensure_ascii=False) + '\n') + + print(f'{len(tasks) - failed}/{len(tasks)} elaborate cleanly') + raise SystemExit(1 if failed else 0) + + +if __name__ == '__main__': + main() diff --git a/textbook/extract_section.py b/textbook/extract_section.py new file mode 100644 index 0000000..bbcfb47 --- /dev/null +++ b/textbook/extract_section.py @@ -0,0 +1,73 @@ +"""Slice one book section out of a `pdftotext -layout` dump and list its labeled +Theorem/Proposition/Lemma/Corollary/Definition statements, as input for formalize.py. + +Produces two files: the section's raw text, and a JSON checklist of labeled items +(kind, label, first line) in book order. The checklist exists so formalize.py's LLM +step has an explicit inventory to cover and cannot silently skip or invent items. +""" +import argparse +import json +import re +from pathlib import Path + +LABEL_RE = re.compile(r'^(Definition|Theorem|Proposition|Lemma|Corollary)\s+(\d+\.\d+(?:\.\d+)?)\.?\s*(.*)$') + + +def find_heading_line(lines, heading): + for i, line in enumerate(lines): + if line.strip() == heading: + return i + raise ValueError(f'Heading not found: {heading!r}') + + +def extract_section(full_text, start_heading, end_heading): + lines = full_text.split('\n') + start = find_heading_line(lines, start_heading) + end = find_heading_line(lines, end_heading) if end_heading else len(lines) + if end <= start: + raise ValueError('end_heading must come after start_heading') + return '\n'.join(lines[start:end]) + + +def labeled_statements(section_text, section_prefix): + """Unique labeled items in section_text whose label starts with section_prefix + (e.g. '1.6.'), keeping only the first occurrence of each label: later matches are + almost always proof continuations across a page break or cross-references, not new + statements. Returned sorted in book order (numeric, not lexical).""" + seen = {} + for line in section_text.split('\n'): + line = line.strip() + m = LABEL_RE.match(line) + if not m: + continue + kind, label, rest = m.group(1), m.group(2), m.group(3) + if not label.startswith(section_prefix) or label in seen: + continue + seen[label] = {"kind": kind, "label": label, "first_line": line[:120]} + + def sort_key(item): + return tuple(int(p) for p in item['label'].split('.')) + + return sorted(seen.values(), key=sort_key) + + +def main(): + parser = argparse.ArgumentParser(description='Slice one section out of a pdftotext -layout dump') + parser.add_argument('layout_txt', type=Path) + parser.add_argument('--start-heading', required=True, help="e.g. '1.6. Divisibility in the Integers'") + parser.add_argument('--end-heading', help="e.g. '1.7. Modular Arithmetic'; omit for end of file") + parser.add_argument('--section-prefix', required=True, help="e.g. '1.6.'") + parser.add_argument('--out-text', type=Path, required=True) + parser.add_argument('--out-index', type=Path, required=True) + args = parser.parse_args() + + full_text = args.layout_txt.read_text(encoding='utf-8') + section_text = extract_section(full_text, args.start_heading, args.end_heading) + args.out_text.write_text(section_text, encoding='utf-8') + index = labeled_statements(section_text, args.section_prefix) + args.out_index.write_text(json.dumps(index, ensure_ascii=False, indent=2) + '\n', encoding='utf-8') + print(f'{len(index)} labeled statements -> {args.out_index}') + + +if __name__ == '__main__': + main() diff --git a/textbook/formalize.py b/textbook/formalize.py new file mode 100644 index 0000000..a7a8f91 --- /dev/null +++ b/textbook/formalize.py @@ -0,0 +1,165 @@ +"""LLM-assisted formalization of a textbook section into Lean 4 candidate statements. + +Reads a section's extracted text and labeled-statement checklist (from +extract_section.py) and asks an LLM to produce: + (a) a Lean 4 theorem statement for every genuine Theorem/Proposition/Lemma/Corollary, + preferring Mathlib's existing vocabulary over reinventing definitions, and + (b) a manifest of every Definition the theorems depend on, pointing at the matching + Mathlib name when one exists and only asking for hand-written Lean `def`s when it + doesn't. + +This step never runs Lean. The extracted PDF text can have corrupted math symbols +(missing =/in, dropped superscripts) from the source PDF's font encoding; the model is +told to lean on its own knowledge of standard textbook mathematics plus the section +context, and to flag low-confidence items rather than guess silently. Always run +check_statements.py against a real Mathlib-backed Lean project before trusting the +output, and before spending lean-agent proof attempts on it. +""" +import argparse +import json +import re +from pathlib import Path + +try: + from .llm import ChatClient, load_dotenv # imported as textbook.formalize +except ImportError: + from llm import ChatClient, load_dotenv # run directly: python3 textbook/formalize.py + +SYSTEM_PROMPT = """You are formalizing a section of an undergraduate abstract algebra \ +textbook (Goodman, "Algebra: Abstract and Concrete") into Lean 4 using Mathlib. + +You will receive: +1. The raw text of one book section, extracted from a PDF. WARNING: the source PDF's \ +math font encoding is broken in this extraction -- symbols like congruence, set \ +membership, comparisons, superscripts and subscripts are frequently dropped or garbled. \ +Use your own knowledge of standard undergraduate number theory / algebra to reconstruct \ +the intended mathematics from context; do not invent content that is not actually in the \ +section. +2. A checklist of every labeled Theorem/Proposition/Lemma/Corollary/Definition in the \ +section (by number), so you know exactly what to cover -- do not skip any, and do not \ +invent ones that are not listed. + +Produce exactly two JSON arrays, "definitions" and "theorems", as a single JSON object \ +inside one ```json fenced code block, and nothing else outside that block. + +Each element of "definitions" (only for Definition-labeled entries the theorems below \ +actually depend on): +{ + "label": "Definition 1.6.3", + "concept": "short name, e.g. 'prime number'", + "mathlib_ref": "Mathlib identifier that already means this, e.g. 'Nat.Prime', or null \ +if Mathlib has no equivalent", + "lean_code": "a standalone Lean 4 `def ...` ONLY if mathlib_ref is null, else null", + "notes": "anything a formalizer should know, e.g. where the book's definition differs \ +from Mathlib's convention" +} + +Each element of "theorems" (one per Theorem/Proposition/Lemma/Corollary in the \ +checklist): +{ + "id": "goodman-1-6-6", + "source_label": "Theorem 1.6.6", + "kind": "theorem", + "statement": "the Lean 4 proposition only, i.e. what goes after `theorem name : `, \ +using Mathlib vocabulary (Nat.Prime, Nat.gcd, Int.gcd, etc.) wherever possible instead \ +of reinventing definitions", + "prelude": "Lean import lines this statement needs, usually just \\"import Mathlib\\"", + "natural_language": "a short original English restatement in your own words (do not \ +quote the source text verbatim)", + "requires": ["list of Mathlib identifiers the statement uses"], + "include_in_bench": true, + "exclude_reason": null +} + +Set "include_in_bench" to false (with a short "exclude_reason") instead of omitting an \ +entry when a checklist item turns out to not be a genuine formalizable claim (e.g. it is \ +actually a definition misfiled under a theorem-style label, a purely numerical one-off \ +computation with no general statement, or the extracted text is too corrupted to recover \ +its meaning confidently) -- still emit the entry so nothing silently disappears, just \ +mark it excluded. + +id must be the label with dots and spaces replaced by hyphens, lowercased, prefixed \ +"goodman-". Do not include a proof, "sorry", or "by" -- statement is only the \ +proposition, no theorem keyword or name. Do not wrap the JSON in anything other than a \ +single ```json fenced block.""" + + +def user_prompt(section_text, checklist): + checklist_lines = '\n'.join(f"- {item['kind']} {item['label']}: {item['first_line']}" + for item in checklist) + return (f"Checklist of labeled items in this section:\n{checklist_lines}\n\n" + f"Section text:\n{section_text}") + + +def extract_json_block(text): + match = re.search(r'```json\s*\n(.*?)```', text, re.S) + payload = match.group(1) if match else text + return json.loads(payload) + + +def validate(data): + if not isinstance(data, dict) or 'theorems' not in data or 'definitions' not in data: + raise ValueError('Response must be a JSON object with "theorems" and "definitions" arrays') + theorems, definitions = data['theorems'], data['definitions'] + if not isinstance(theorems, list) or not isinstance(definitions, list): + raise ValueError('"theorems" and "definitions" must be arrays') + seen_ids = set() + for item in theorems: + for field in ('id', 'source_label', 'statement', 'prelude', 'include_in_bench'): + if field not in item: + raise ValueError(f'theorem entry missing field {field!r}: {item}') + if item['id'] in seen_ids: + raise ValueError(f'Duplicate theorem id: {item["id"]}') + seen_ids.add(item['id']) + for item in definitions: + for field in ('label', 'concept', 'mathlib_ref'): + if field not in item: + raise ValueError(f'definition entry missing field {field!r}: {item}') + return theorems, definitions + + +def main(): + parser = argparse.ArgumentParser(description='LLM-formalize a book section into Lean 4 candidate statements') + parser.add_argument('section_text', type=Path) + parser.add_argument('statement_index', type=Path) + parser.add_argument('--out-dataset', type=Path, required=True, help='JSONL of theorems with include_in_bench=true') + parser.add_argument('--out-definitions', type=Path, required=True, help='JSON manifest of definitions') + parser.add_argument('--out-excluded', type=Path, help='JSONL of theorem entries the model excluded, for review') + parser.add_argument('--model', required=True) + parser.add_argument('--base-url', default='https://dashscope.aliyuncs.com/compatible-mode/v1') + parser.add_argument('--api-key-env', default='DASHSCOPE_API_KEY') + parser.add_argument('--env-file', type=Path, default=Path(__file__).resolve().parents[1] / '.env') + parser.add_argument('--timeout', type=float, default=300) + args = parser.parse_args() + + load_dotenv(args.env_file) + client = ChatClient(args.model, args.base_url, args.api_key_env, args.timeout) + checklist = json.loads(args.statement_index.read_text(encoding='utf-8')) + section_text = args.section_text.read_text(encoding='utf-8') + messages = [{"role": "system", "content": SYSTEM_PROMPT}, + {"role": "user", "content": user_prompt(section_text, checklist)}] + reply = client.complete(messages) + data = extract_json_block(reply) + theorems, definitions = validate(data) + + included = [t for t in theorems if t.get('include_in_bench')] + excluded = [t for t in theorems if not t.get('include_in_bench')] + + with args.out_dataset.open('w', encoding='utf-8') as stream: + for item in included: + stream.write(json.dumps(item, ensure_ascii=False) + '\n') + args.out_definitions.write_text(json.dumps(definitions, ensure_ascii=False, indent=2) + '\n', encoding='utf-8') + if args.out_excluded: + with args.out_excluded.open('w', encoding='utf-8') as stream: + for item in excluded: + stream.write(json.dumps(item, ensure_ascii=False) + '\n') + + print(f'{len(included)} theorems -> {args.out_dataset}') + if excluded: + note = f' (see {args.out_excluded})' if args.out_excluded else ' (pass --out-excluded to keep them)' + print(f'{len(excluded)} excluded{note}') + print(f'{len(definitions)} definitions -> {args.out_definitions}') + + +if __name__ == '__main__': + main() diff --git a/textbook/llm.py b/textbook/llm.py new file mode 100644 index 0000000..6a6d299 --- /dev/null +++ b/textbook/llm.py @@ -0,0 +1,46 @@ +"""Minimal OpenAI-compatible chat client, standalone (no third-party deps, no import of +lean_agent) so this pipeline works regardless of whether lean-agent is pip-installed. +Mirrors lean_agent.core.HTTPProvider on purpose; kept separate deliberately.""" +import json +import os +import urllib.request + + +def load_dotenv(path): + """Load KEY=VALUE lines from a .env file into os.environ (does not overwrite vars + already set). Silently does nothing if the file does not exist.""" + if not path.exists(): + return + for line in path.read_text(encoding='utf-8').splitlines(): + line = line.strip() + if not line or line.startswith('#') or '=' not in line: + continue + key, _, value = line.partition('=') + key = key.strip() + value = value.strip().strip('"').strip("'") + os.environ.setdefault(key, value) + + +class ChatClient: + """OpenAI-compatible /chat/completions caller.""" + + def __init__(self, model, base_url, api_key_env='DASHSCOPE_API_KEY', timeout=300): + self.model = model + self.base_url = base_url.rstrip('/') + self.api_key_env = api_key_env + self.timeout = timeout + + def complete(self, messages, temperature=0.2): + key = os.environ.get(self.api_key_env) + if not key: + raise RuntimeError(f'Missing API key in environment variable {self.api_key_env}') + headers = {"Content-Type": "application/json", "Authorization": "Bearer " + key} + payload = {"model": self.model, "messages": messages, "temperature": temperature} + request = urllib.request.Request(self.base_url + '/chat/completions', + data=json.dumps(payload).encode(), headers=headers) + with urllib.request.urlopen(request, timeout=self.timeout) as response: + data = json.load(response) + content = data["choices"][0]["message"]["content"] + if not isinstance(content, str): + raise ValueError("Provider returned non-text content") + return content diff --git a/textbook/section_1_6.index.json b/textbook/section_1_6.index.json new file mode 100644 index 0000000..da9a3fd --- /dev/null +++ b/textbook/section_1_6.index.json @@ -0,0 +1,117 @@ +[ + { + "kind": "Proposition", + "label": "1.6.1", + "first_line": "Proposition 1.6.1." + }, + { + "kind": "Proposition", + "label": "1.6.2", + "first_line": "Proposition 1.6.2. Let a, b, c, u, and v denote integers." + }, + { + "kind": "Definition", + "label": "1.6.3", + "first_line": "Definition 1.6.3. A natural number is prime if it is greater than 1 and not" + }, + { + "kind": "Proposition", + "label": "1.6.4", + "first_line": "Proposition 1.6.4. Any natural number other than 1 can be written as a" + }, + { + "kind": "Theorem", + "label": "1.6.6", + "first_line": "Theorem 1.6.6. There are infinitely many prime numbers." + }, + { + "kind": "Proposition", + "label": "1.6.7", + "first_line": "Proposition 1.6.7. Given integers a and d , with d \u0015 1, there exist unique" + }, + { + "kind": "Definition", + "label": "1.6.8", + "first_line": "Definition 1.6.8. A natural number d is the greatest common divisor of" + }, + { + "kind": "Proposition", + "label": "1.6.9", + "first_line": "Proposition 1.6.9. For integers n and m, let" + }, + { + "kind": "Lemma", + "label": "1.6.10", + "first_line": "Lemma 1.6.10. Let m and n be nonzero integers. If a natural number d" + }, + { + "kind": "Proposition", + "label": "1.6.11", + "first_line": "Proposition 1.6.11. The natural number nr is the greatest common divisor" + }, + { + "kind": "Corollary", + "label": "1.6.13", + "first_line": "Corollary 1.6.13. Let m and n be nonzero integers, and write d D" + }, + { + "kind": "Definition", + "label": "1.6.14", + "first_line": "Definition 1.6.14. Nonzero integers m and n are relatively prime if" + }, + { + "kind": "Corollary", + "label": "1.6.15", + "first_line": "Corollary 1.6.15. Two nonzero integers m and n are relatively prime if" + }, + { + "kind": "Corollary", + "label": "1.6.17", + "first_line": "Corollary 1.6.17. Suppose that a and b are relatively prime natural num-" + }, + { + "kind": "Proposition", + "label": "1.6.18", + "first_line": "Proposition 1.6.18. If p is a prime number and a is any nonzero integer," + }, + { + "kind": "Proposition", + "label": "1.6.19", + "first_line": "Proposition 1.6.19. Let p be a prime number, and a and b nonzero inte-" + }, + { + "kind": "Corollary", + "label": "1.6.20", + "first_line": "Corollary 1.6.20. Suppose that a prime number p divides a product" + }, + { + "kind": "Theorem", + "label": "1.6.21", + "first_line": "Theorem 1.6.21. The prime factorization of a natural number is unique." + }, + { + "kind": "Definition", + "label": "1.6.22", + "first_line": "Definition 1.6.22. A natural number d is the greatest common divisor of" + }, + { + "kind": "Lemma", + "label": "1.6.23", + "first_line": "Lemma 1.6.23. Given nonzero integers a1 ; a2 ; : : : ; an (n \u0015 2), there is a" + }, + { + "kind": "Proposition", + "label": "1.6.24", + "first_line": "Proposition 1.6.24. The greatest common divisor of nonzero inte-" + }, + { + "kind": "Definition", + "label": "1.6.25", + "first_line": "Definition 1.6.25. We say that non-zero integers a1 ; : : : ; an are relatively" + }, + { + "kind": "Lemma", + "label": "1.6.26", + "first_line": "Lemma 1.6.26. Let a1 ; : : : ; an be pairwise relatively prime integers, and" + } +]