Meta与NYU论文：简单循环配合Lean工具超越人工定理证明工作流
New Meta, NYU paper shows that a simple loop with good Lean tools and more compu…
这篇论文揭示了无需复杂规划的工作流也能在数学证明上超越人工设计，对 Agent 架构设计有直接参考价值，建议关注其循环机制细节。
New Meta, NYU paper shows that a simple loop with good Lean tools and more compute matches or beats hand-built theorem-proving workflows.
Meta与纽约大学（NYU）的论文表明，一个配备良好Lean工具和更多算力的简单循环，能够匹配或超越手工构建的定理证明工作流。
Systems that write math proofs in Lean, a language a computer can check, increasingly use hand-designed workflows that plan and split up problems. Their gains often come with stronger models or more compute, hiding what the workflow adds.
使用Lean语言编写数学证明的系统日益增多，这是一种计算机可验证的语言，这些系统越来越多地采用人工设计的工作流来规划和分解问题。其性能提升往往伴随着更强模型或更多算力的投入，从而掩盖了工作流本身带来的贡献。
They built h1, a loop that gives the model fast Lean feedback and search tools, and keeps it working after each failed check. It imposes no plan, only a progress summary before each new round.
他们构建了h1，这是一个为模型提供快速Lean反馈和搜索工具的循环机制，并在每次检查失败后保持模型继续运行。它不施加任何计划，仅在新的一轮开始前提供进度摘要。
With the same model, h1 beat the hand-built Goedel-Architect on PutnamBench, 598 problems to 597, at $1.08 against $1.47 per problem. The interface still matters: with Opus 4.8, h1 solved 83 of 100 hard algebra problems, against 63 for Claude Code.
在相同模型下，h1在PutnamBench基准测试中以598题对597题的成绩击败了手工构建的Goedel-Architect，单题成本为1.08美元，低于后者的1.47美元。界面仍然至关重要：在使用Opus 4.8时，h1解决了100道高难度代数题中的83道，而Claude Code仅解决了63道。
更进一步：量化金融体系
看懂新闻只是起点——沿量化金融路径，把它变成能交付的工程能力