ZkGolf开源零知识电路竞赛 验证Lean 4证明

zkGolf 深度解读：用 Lean 4 零知识电路“打高尔夫”竞赛

背景

零知识（Zero-Knowledge）电路是区块链与密码学领域核心技术，负责将复杂计算转化为可证明的约束系统，实现隐私保护计算（如零知识证明）。传统电路编写依赖手工优化或专用 DSL（如 Circom），效率低、验证难。Lean 4 作为现代证明辅助工具，已被 zksecurity 等团队用于形式化验证 ZK 电路，提供机器可读的精确数学语义。

zkGolf 正是这一趋势的产物。它由 zksecurity 团队发起，定位为社区竞赛平台，目标是推动“最廉价”（cheapest）零知识电路的开发与形式化验证。赛程始于 2025 年底，旨在将电路优化推向极致，同时确保“已证明正确”。平台同时支持传统人类开发者与 AI 代理参与，通过标准化 API 实现“自动研究”（autoresearch）。

核心内容

zkGolf 是一个明确定义的竞赛机制：参赛者从公开挑战（challenge）中选取一项，编写 Lean 4 电路，实现更高效的约束系统，并通过 Lean 证明其正确性与合规性。

核心流程：

1. 选手（或 AI 代理）读取公开挑战规范，包括接口定义（Interface.lean）、规范文件（Specs）与配置。
2. 编写新的 Lean 电路实现（通常包含 Main.lean 等入口文件）。
3. 使用 Lean 4 完成证明：展示电路逻辑等价于规范，并验证所有约束被正确满足。
4. 提交方案（submission）：包含代码文件、声明的电路成本（allocations + constraints），以及可选的辅助模型标注。
5. 平台验证：自动构建并运行形式化检查器（Comparator），确认证明有效、无违背规范。验证通过后，按成本得分（allocations + constraints），成本越低排名越高。

平台支持 3 个初始公开挑战（基于 zk-golf-challenges 项目仓库），包括：

• AssertBytes：断言字节级操作的正确性验证。
• SHA256：哈希函数电路实现。
• RSASSAPKCS1v15_SHA256_4096_65537：RSA PKCS#1 v1.5 签名验证电路（采用 4096 位密钥）。

提交必须使用 pinned Lean 版本、受限的证明表面（禁止 native_decide 等超参数），并在本地验证后方可上传。平台提供专用 Agent API（OpenAPI 规范），包括挑战列表、排行榜、提交 POST 接口及验证日志查询。挑战源码以 tarball 形式提供，便于本地开发。

/llms.txt 文件专门为 AI 代理设计，包含机器可读的使用指南、API 参考、如何读取挑战、编写电路及提交解决方案的详细说明。整个平台强调“本地优先验证”：未经本地通过的提交将被拒绝。

关键要点

• 唯一评分指标为“成本”（allocations + constraints），目标是突破基准（par）得分，越低越好，领先者获“最高分”排名。
• 所有提交需用 Lean 4 形式化证明电路等价于规范，无需手动证明正确性，降低人为错误。
• 平台内置对 AI 代理的完全支持：/llms.txt 提供标准化接口，允许代理独立读取挑战、生成代码、提交解决方案并获取验证日志。
• 限制严格：使用固定依赖版本、受限证明公理、本地验证优先，防止超时或恶意提交。
• 3 个公开挑战涵盖常见 ZK 电路场景（断言、哈希、签名），为开发与优化提供具体目标。

意义与影响

zkGolf 首次将零知识电路优化推向“竞赛”维度，将传统工程实践转化为可度量、可比较的竞技项目，推动社区形成共识：最优电路不仅依赖领域知识，更依赖形式化证明与代码验证能力。

对开发者而言，它为机器可读的电路设计提供了参考示例，加速从手工到 AI 辅助的转型。AI 代理通过 /llms.txt 与专用 API 实现“全自动”参与，代表了“autoresearch”在密码学领域的首个落地案例，有望降低传统电路开发门槛。

从技术角度，平台强制形式化验证，减少了 ZK 电路常见的 under-constrained 或非确定性问题，提高了协议安全性。对于区块链、隐私计算和形式化方法社区，zkGolf 提供了可扩展的基准测试框架，未来可能扩展更多挑战，标准化学术电路优化。

总体而言，zkGolf 不是单纯的竞赛，而是桥梁：连接人类创意的极致优化与 AI 代理的自动化验证，共同推进零知识技术向更高效、更可靠的方向演进。