From 99638be63747c144e836fad2e20b80fa92993b57 Mon Sep 17 00:00:00 2001
From: Codex Bot <codex-bot@gitea.entroia.local>
Date: Tue, 15 Sep 2026 19:15:05 +0800
Subject: [PATCH] Implement provider-neutral Lean reasoning and evaluation
 foundation

---
 .gitignore             |  5 +++++
 README.md              | 28 +++++++++++++++++++++++
 datasets/smoke.jsonl   |  3 +++
 lean-toolchain         |  1 +
 lean_bench/__init__.py |  0
 lean_bench/cli.py      | 50 ++++++++++++++++++++++++++++++++++++++++++
 pyproject.toml         | 16 ++++++++++++++
 tests/mock_provider.py |  3 +++
 tests/test_dataset.py  | 11 ++++++++++
 9 files changed, 117 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 README.md
 create mode 100644 datasets/smoke.jsonl
 create mode 100644 lean-toolchain
 create mode 100644 lean_bench/__init__.py
 create mode 100644 lean_bench/cli.py
 create mode 100644 pyproject.toml
 create mode 100644 tests/mock_provider.py
 create mode 100644 tests/test_dataset.py

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..2c255f8
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,5 @@
+__pycache__/
+*.egg-info/
+.venv/
+.env
+results/
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..d91479f
--- /dev/null
+++ b/README.md
@@ -0,0 +1,28 @@
+# Lean Bench
+
+独立评测项目，依赖 lean-agent；两者放在同一父目录。
+
+```sh
+python3 -m venv .venv
+source .venv/bin/activate
+pip install -e ../lean-agent -e .
+export LLM_API_KEY='your-key'
+lean-bench datasets/smoke.jsonl --output results/model-001 --model YOUR_MODEL --base-url https://YOUR_HOST/v1 --attempts 3
+```
+
+也支持 agent 的 --provider-command、--lean-project、--lean-command 和超时选项。协议见 [Lean Agent](https://gitea.entroia.com/codex-bot/lean-agent)。
+
+输入 JSONL 每行包含唯一 id、statement，可选 prelude。数据集必须可信；拒绝空集、重复 ID 和缺少字段。
+
+输出目录必须不存在：results.jsonl 逐题记录证明、Lean 诊断、耗时和错误；summary.json 汇总成功率、异常数、尝试数、模型、Lean 版本及数据集 SHA-256。异常题保留在分母。指标为修复预算内 solved/tasks，不是独立采样 pass@k。顺序运行，暂不支持断点续跑。
+
+不同实验应固定模型、预算、Lean/Mathlib、数据集与适配器版本。三个 smoke 题只验证流程，不代表数学推理能力。
+
+## 无 LLM 的真实 Lean smoke 测试
+
+```sh
+lean-bench datasets/smoke.jsonl --output results/smoke-001 --provider-command '["python3","tests/mock_provider.py"]'
+python3 -m unittest discover -s tests -v
+```
+
+mock 返回固定证明，仍由真实 Lean 检查。真实 LLM 需配置 endpoint/model 或适配器。
diff --git a/datasets/smoke.jsonl b/datasets/smoke.jsonl
new file mode 100644
index 0000000..b8ff2e6
--- /dev/null
+++ b/datasets/smoke.jsonl
@@ -0,0 +1,3 @@
+{"id": "nat-refl", "statement": "\u2200 n : Nat, n = n"}
+{"id": "and-swap", "statement": "\u2200 p q : Prop, p \u2227 q \u2192 q \u2227 p"}
+{"id": "add-zero", "statement": "\u2200 n : Nat, n + 0 = n"}
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000..a8afa7d
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.33.1
diff --git a/lean_bench/__init__.py b/lean_bench/__init__.py
new file mode 100644
index 0000000..e69de29
diff --git a/lean_bench/cli.py b/lean_bench/cli.py
new file mode 100644
index 0000000..725c045
--- /dev/null
+++ b/lean_bench/cli.py
@@ -0,0 +1,50 @@
+"""JSONL benchmark runner; failed tasks stay in the denominator."""
+import argparse
+import hashlib
+import json
+import subprocess
+from pathlib import Path
+from lean_agent.cli import options, components
+from lean_agent.core import solve
+
+def load_tasks(path):
+    tasks = [json.loads(line) for line in path.read_text().splitlines() if line.strip()]
+    seen = set()
+    for task in tasks:
+        if not isinstance(task.get('id'), str) or not isinstance(task.get('statement'), str):
+            raise ValueError('Every task needs string id and statement')
+        if task['id'] in seen: raise ValueError('Duplicate task id: ' + task['id'])
+        seen.add(task['id'])
+    if not tasks: raise ValueError('Empty dataset')
+    return tasks
+
+def main():
+    parser = argparse.ArgumentParser(description='Evaluate Lean agent on trusted JSONL tasks')
+    parser.add_argument('dataset', type=Path)
+    parser.add_argument('--output', type=Path, required=True, help='New directory for this run')
+    options(parser)
+    args = parser.parse_args()
+    if args.attempts < 1: parser.error('--attempts must be positive')
+    tasks = load_tasks(args.dataset)
+    provider, verifier = components(args)
+    args.output.mkdir(parents=True, exist_ok=False)
+    version = subprocess.run([*verifier.command, '--version'], cwd=verifier.cwd,
+                             capture_output=True, text=True, timeout=30).stdout.strip()
+    passed = errors = total_attempts = 0
+    with (args.output / 'results.jsonl').open('w') as stream:
+        for task in tasks:
+            result = solve(provider, verifier, task, args.attempts)
+            passed += result['success']
+            errors += 'error' in result
+            total_attempts += len(result['attempts'])
+            stream.write(json.dumps(result, ensure_ascii=False) + '\n')
+            stream.flush()
+    summary = {'tasks': len(tasks), 'solved': passed, 'solve_rate': passed / len(tasks),
+               'errors': errors, 'attempts': total_attempts, 'max_attempts': args.attempts,
+               'model': args.model, 'provider': 'command' if args.provider_command else 'http',
+               'lean_version': version,
+               'dataset_sha256': hashlib.sha256(args.dataset.read_bytes()).hexdigest()}
+    (args.output / 'summary.json').write_text(json.dumps(summary, indent=2) + '\n')
+    print(json.dumps(summary, indent=2))
+
+if __name__ == '__main__': main()
diff --git a/pyproject.toml b/pyproject.toml
new file mode 100644
index 0000000..7c46ee0
--- /dev/null
+++ b/pyproject.toml
@@ -0,0 +1,16 @@
+[build-system]
+requires = ["setuptools>=68"]
+build-backend = "setuptools.build_meta"
+
+[project]
+name = "lean-bench"
+version = "0.1.0"
+requires-python = ">=3.11"
+description = "Provider-independent Lean reasoning benchmark"
+dependencies = ["lean-agent>=0.1.0,<0.2"]
+
+[project.scripts]
+lean-bench = "lean_bench.cli:main"
+
+[tool.setuptools.packages.find]
+include = ["lean_bench*"]
diff --git a/tests/mock_provider.py b/tests/mock_provider.py
new file mode 100644
index 0000000..03aeb38
--- /dev/null
+++ b/tests/mock_provider.py
@@ -0,0 +1,3 @@
+import json, sys
+s = json.load(sys.stdin)["messages"][1]["content"]
+print("intro p q h; exact And.intro h.right h.left" if "∧" in s else "intro n; rfl")
diff --git a/tests/test_dataset.py b/tests/test_dataset.py
new file mode 100644
index 0000000..fa88afd
--- /dev/null
+++ b/tests/test_dataset.py
@@ -0,0 +1,11 @@
+import tempfile
+import unittest
+from pathlib import Path
+from lean_bench.cli import load_tasks
+class Tests(unittest.TestCase):
+    def test_duplicate(self):
+        with tempfile.TemporaryDirectory() as directory:
+            path = Path(directory)/'data.jsonl'
+            path.write_text('{"id":"x","statement":"True"}\n' * 2)
+            with self.assertRaises(ValueError): load_tasks(path)
+if __name__ == '__main__': unittest.main()