主要证据
- Long-horizon autoformalization of a core theorem underlying MIP* = RES1 · 主要研究来源 · 论文 · 2026-09-17
- MIPStarRE Lean formalization repositoryS1 · 主要研究来源 · 形式化工件
FormalFlow 完成支撑 MIP* = RE 核心定理的 12.6 万行 Lean 形式化
FormalFlow 以共享 blueprint 为核心，将长程形式化组织为嵌套的规划、证明与审查循环。 AI Agent 负责实现和审查证明任务，人类则监督整体项目、对照形式化开发与原始数学文本， 并处理语义偏差。公开的 MIPStarRE 仓库保存 Lean 源码、活动 blueprint、源论文材料 以及面向 CI 的证明完整性基础设施。
发生了什么？
FormalFlow 团队报告完成经典低个体次数测试 quantum soundness 定理的完整 Lean 4 机器检查证明；该定理是 MIP* = RE 研究路线中的核心定理之一。论文报告该开发历时 63 天，包含 126,367 行由 AI 证明 Agent 生成的 Lean 代码，并在保持修正后假设下 最终误差界不变的同时，纠正了若干边界条件与中间错误。
为什么重要？
大型研究证明会暴露短题 benchmark 难以体现的问题，包括 statement drift、依赖管理、 局部 lemma 不兼容与长期审查债务。FormalFlow 表明，Agent 工作流可以在数月尺度上 持续推进研究级形式化，并把 Lean kernel 作为最终形式证明检查层，同时通过额外项目 流程审查形式陈述与原始数学之间的语义忠实度。
重要性说明：FormalFlow 构成长程 AI 辅助形式化方向的领域级里程碑：它报告完成了经典低个体次数 测试 quantum soundness 定理的 Lean 机器检查形式化，而该定理是 MIP* = RE 证明 体系中的核心技术组成。项目历时 63 天，形成 126,367 行由证明 Agent 生成、在人类 监督下完成的 Lean 代码，体现了远超单个 proof hole 求解的持续规划、组合与审查能力； 但其核心贡献是已知研究证明的形式化，而不是新的数学定理。
历史脉络
更早进展
—
后续进展
—
相关里程碑
—
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- 人机协作
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 已知结果形式化
- 接口
- 形式化, 混合
- AI 贡献
- 论文表示 Lean 代码库由 FormalFlow 协调的 AI 证明 Agent 生成；人类负责项目监督， 并参与规划、源数学忠实度审查以及证明或陈述缺口的处理。
- 人类贡献
- 人类研究者设计并监督工作流、选择和解释目标定理、维护 blueprint 与审查流程， 并处理论文与形式化开发之间的语义差异。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 机器检查
- 最后审阅
- 2026-09-27
技术细节
- 系统
- formalflow, lean
- 机构
- —
- 数学问题
- mip-star-equals-re, low-individual-degree-test
- 方法
- long-horizon-autoformalization, multi-agent-proof-development, blueprint-guided-formalization, formal-verification
全部来源与工件
- Long-horizon autoformalization of a core theorem underlying MIP* = RES1 · 主要研究来源 · 论文 · 访问于 2026-09-27
- MIPStarRE Lean formalization repositoryS1 · 主要研究来源 · 形式化工件 · 访问于 2026-09-27
- MIPStarRE Lean 4 development工件 · 证明工件
验证历史
- 2026-09-17 · 论文已发布 · E3 · 可检查工件
arXiv 论文报告已完成 Lean 4 机器检查形式化，公开 MIPStarRE 仓库提供相应 Lean 工程及证明开发基础设施。本轮维护尚未发现针对该发布成果的独立重放记录。
更正
当前没有记录的更正。