h1 在自动定理证明中体现“苦涩教训”：简单智能体循环的潜力

h1 证明简单的智能体循环加上 Lean 4 高效接口，能匹敌人类设计的工作流。 在 PutnamBench 等基准测试中达到最先进水平，解决 8 个 FormalConjectures 未解问题。 该研究建议在评估前沿模型时优先考虑高效的执行反馈机制。