数学与形式推理
突破级
暂无讲解视频
收录解读
这篇论文抓住了 theorem-proving agent 的一个长期瓶颈：证明过程中产生的中间结果往往是一次性的，既不稳定，也不容易沉淀成跨题目可复用的知识资产。DreamProver 用 wake-sleep 循环把这个问题转成 lemma library 的持续演化。
它的价值不在某个 benchmark 多赢几分，而在提供了一个更 durable 的 formal reasoning workflow：proof attempts 不只是为了过当前题，还会反哺出更抽象、可迁移的 lemma 库，形成后续证明的 reusable substrate。
它值得正式收录，因为这已经接近数学 agent 的 memory / knowledge accumulation primitive，而不是一次性策略搜索技巧。对 theorem proving、formal verification、program induction 都有外溢。
它没有更高，是因为当前仍主要停留在 lemma-library 演化这一层，距离更完整的 autonomous math research stack 还有结构距离。