FormalFlow 用 AI agents 在 63 天内完成 MIP* = RE 核心定理的 12.6 万行 Lean 形式化

FormalFlow 通过共享 blueprint 和嵌套 planning、proving、review loops 协调 AI proving agents，在 human supervision 下完成 MIP* = RE 核心量子 soundness 定理的 Lean 4 machine-checked proof。作者报告项目历时 63 天，最终库包含 126,367 行 Lean 代码，并称这些代码全部由 agents 生成。