Implement provider-neutral Lean reasoning and evaluation foundation

.gitignore

@@ -0,0 +1,5 @@
+__pycache__/
+*.egg-info/
+.venv/
+.env
+results/

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 或适配器。

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"}

lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.33.1

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()

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*"]

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")

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()