本地证明闭环
Verifier-Guided Multi-Round Lean Proof Loop

项目简介 • 功能特性 • 快速开始 • 文档 • 代码结构 • 生态位置 • 贡献 • English

围绕“形式化证明多轮闭环”构建的本地主机-客户端系统：支持验证、反馈与迭代求解。

---

项目简介

“人—智能体混合数字世界”的一个关键问题是：
如果我们希望智能体在一个公共环境中持续解决真实问题，那么系统必须提供稳定的任务发布、客观验证、结构化反馈与多轮收敛机制。

本项目对应其中的形式化证明闭环层，负责解决“用户侧 agent 如何在统一 verifier 下，多轮地向正确证明收敛”这个问题。
没有这一层，智能体在数学证明场景中往往只能一次性输出代码片段；有了这一层，证明生成就能被组织成“提交候选证明 -> 形式验证 -> 返回诊断 -> 再次尝试”的服务化过程。

核心思想

• 验证先于叙述：证明是否成立由 Lean verifier 决定，而不是由模型自我判断。
• 客户端/服务端分离：solver 像客户端一样提交尝试，host 像服务一样统一执行验证与调度。
• 多轮收敛而非一次生成：把形式化证明视作 verifier-guided iterative synthesis，而不是单轮代码生成。

适合以下场景与读者

• 研究者：希望研究多轮形式化证明 agent 的行为与收敛性
• 平台设计者：希望把 proof loop 接入竞技场或评测系统
• 工程师：需要一个最小可跑的 host/client 证明闭环原型
• 产品探索者：关注他山世界、公众科学、协作式形式化数学方向

---

功能特性

• Hermes solver skill：用户侧 agent 读取 solver packet，生成 body_only 证明提交。
• Codex orchestrator skill：服务侧 agent 发布 run、推进状态、在需要时路由 reviewer。
• 确定性 Lean 执行：由 Python host runner 负责模板注入、编译执行与规则检查。
• HTTP 外部协议：支持 publish / submit / process / review / status。
• 样例题包与 fixtures：提供立即成功、正常 retry、forbidden-pattern stop 三种路径。

---

快速开始

1. 准备 Lean 项目根目录

export LEAN_PROJECT_ROOT=/abs/path/to/your/lean/project

2. 启动本地 HTTP 服务

cd /path/to/local-proof-loop
python3 scripts/local_loop_http.py --host 127.0.0.1 --port 8788

3. 发布一轮任务

curl -s http://127.0.0.1:8788/publish \
  -H 'content-type: application/json' \
  -d '{"problem_id":"minif2f_mathd_algebra_478"}'

4. 用 Hermes 求解

Use local-proof-loop-solver with http://127.0.0.1:8788 on problem minif2f_mathd_algebra_478 and keep solving until the host returns complete, stop, or another round packet.

5. 用 Codex 推进 host 侧状态

Use local-proof-loop-orchestrator with http://127.0.0.1:8788 on run minif2f_mathd_algebra_478/run_001 and process the current state until the host either needs Hermes again or terminates.

---

文档

文档	说明
docs/external-protocol.md	外部 client/server 协议
docs/local-http-api.md	本地 HTTP 接口说明
docs/dependencies.md	依赖与环境要求
docs/install-skills.md	skill 安装方式
docs/roadmap.md	从本地原型走向竞技场与公众科学的路线图

---

代码结构

local-proof-loop/
├── docs/                    # 协议、依赖、路线图等文档
│   └── assets/              # README 静态资源（Logo 等）
├── problems/                # 打包后的 theorem problem
├── schemas/                 # JSON schema 契约
├── scripts/                 # host runner、local runner、HTTP facade
├── skills/                  # 仓库内 skill 源文件
│   ├── solver/              # Hermes solver skill
│   ├── orchestrator/        # Codex orchestrator skill
│   └── reviewer/            # 可选 reviewer skill
├── README.md                # 中文说明
├── README.en.md             # 英文说明
├── CONTRIBUTING.md          # 贡献说明
├── CHANGELOG.md             # 更新日志
└── LICENSE                  # MIT License

关键脚本

• scripts/host_runner.py：确定性 Lean 执行
• scripts/local_loop_runner.py：内部文件状态机
• scripts/local_loop_http.py：HTTP facade

---

生态位置

本项目是“人—智能体混合数字世界”大项目中的一个底层技术原型，负责验证“形式化证明多轮收敛闭环”。

人—智能体混合数字世界
├── 世界/平台层
│   ├── Tashan World / Arcade（任务发布与竞技场）  ← 未来接入方向
│   └── 公共协作层（公众科学 / formal math）       ← 更长期方向
├── 智能体交互层
│   ├── 用户侧 solver agent
│   └── 服务侧 orchestrator / reviewer
└── 形式验证基础设施层
    └── Local Proof Loop ★ 本仓库

相关仓库 / 方向

仓库 / 方向	定位	链接
TashanGKD/local-proof-loop	当前仓库，本地 proof loop 原型	当前页面
Tashan World / Arcade	未来任务发布与竞技场入口	待接入
公共协作数学层	更长期的公众科学方向	待建

---

贡献

欢迎贡献！详见 CONTRIBUTING.md。

• 代码贡献：请优先保持协议边界清晰，并为 runner 行为提供可复现验证步骤
• 文档贡献：欢迎补充协议文档、README、样例题说明

---

更新日志

版本变更见 CHANGELOG.md。

---

许可证

MIT License. See LICENSE for details.