精选理由
形式化定理证明一直门槛高、成本高，Goedel-Architect 用蓝图+精炼策略大幅提升效率，做数学证明或形式化验证的团队值得关注，开源且成本极低。
Goedel-Architect 是一个基于 Lean 4 的智能体框架，通过生成和精炼“蓝图”（定义和引理的依赖图）来简化形式化定理证明。它先根据自然语言证明生成蓝图，然后并行证明每个引理节点，失败节点会驱动全局蓝图精炼，避免了传统递归分解的低效循环。使用开源模型 DeepSeek-V4-Flash 作为骨干，在 MiniF2F-test 上达到 99.2% pass@1，在 PutnamBench 上达到 75.6% pass@1。结合自然语言证明引导，可解决更难的题目，如 IMO 2025 的 4/6 和 Putnam 2025 的 11/12。该框架在开源管道中实现了最先进性能，且成本比同类开源方案低 500 倍。
AI 翻译 · 中文
Goedel-Architect 是一个基于 Lean 4 的智能体框架，通过生成和精炼“蓝图”（定义和引理的依赖图）来简化形式化定理证明。它先根据自然语言证明生成蓝图，然后并行证明每个引理节点，失败节点会驱动全局蓝图精炼，避免了传统递归分解的低效循环。使用开源模型 DeepSeek-V4-Flash 作为骨干，在 MiniF2F-test 上达到 99.2% pass@1，在 PutnamBench 上达到 75.6% pass@1。结合自然语言证明引导，可解决更难的题目，如 IMO 2025 的 4/6 和 Putnam 2025 的 11/12。该框架在开源管道中实现了最先进性能，且成本比同类开源方案低 500 倍。
We introduce Goedel-Architect, an agentic framework for formal theorem proving in Lean 4 centered on blueprint generation and refinement. A blueprint is a dependency graph of definitions and lemmas that builds up to the …
- Pandaily06-06 07:35原文