MIP* = RE核心定理的长时程自动形式化
Long-horizon autoformalization of a core theorem underlying MIP* = RE
浏览论文内容
中文总结 AI 辅助
FormalFlow系统通过人类监督下的AI证明代理协作，在63天内完成了MIP* = RE核心定理的Lean 4机器检查证明，生成了126,367行代码，为量子复杂性提供了验证基础。
中文摘要 AI 辅助
里程碑式的数学形式化工作往往需要专家团队数年时间才能完成。我们提出了FormalFlow，一个在人类监督下协调AI证明代理的系统，以解决长周期形式化中的陈述漂移和证明组合问题。该系统借鉴软件工程的原则和实践，使用共享蓝图来指导嵌套的规划、证明和审查循环。代理在整个形式化过程中加强验证和审查。我们完成了经典低个体度测试的量子可靠性的机器检查Lean 4证明，这是MIP* = RE背后的一个核心定理。开发该证明耗时63天；更高的并行度可进一步缩短此时间。最终库包含126,367行Lean代码，全部由代理生成。该形式化修正了附带条件和中间错误，同时在修正后的假设下保留了已发表的最终误差界。这项工作为量子复杂性提供了经过验证的基础，并展示了小团队以可负担成本验证重大研究证明的途径。
英文摘要
Landmark mathematical formalizations have taken specialist teams years to complete. We present FormalFlow, a system that coordinates AI proving agents under human supervision to address statement drift and proof composition in long-horizon formalization. Drawing on software engineering principles and practices, it uses a shared blueprint to guide nested planning, proving and review loops. Agents strengthen verification and review throughout formalization. We completed a machine-checked Lean 4 proof of the quantum soundness of the classical low individual-degree test, a core theorem underlying MIP* = RE. Developing the proof took 63 days; greater parallelism could further reduce this time. The final library contains 126,367 lines of Lean code, all generated by agents. The formalization corrects side conditions and intermediate errors while preserving the published final error bound under corrected assumptions. This work provides a verified foundation for quantum complexity and demonstrates a route to affordable verification of major research proofs by small teams.
发表机构
- Munich Center for Quantum Science and Technology (MCQST)（慕尼黑量子科学与技术中心）
- Tsinghua University（清华大学）
机构由 AI 辅助整理，请以论文原文为准。
