Anthropic 实际发布了什么
设定：“数十个 Claude 智能体协作定义概念、证明中间定理，并利用这些定理证明更难的命题。”测试框架基于 Claude Code，运行消耗了“来自一个通用内部研究模型（大致相当于 Claude Fable 5.1）的约 60 亿个输出 token”。人类的数学输入微乎其微——Anthropic 引用了仅有的几条指令：“雅可比矩阵作为方案听起来优先级很高”，“推动 [Mazur 定理] 尽快完成”。
接着是失败与修复。“当我们转向使用 Prove2Me 时，这项工作取得了成功。Prove2Me 是由哥伦比亚大学的彭天翼及其合作者设计的一个用于数学形式化的开放式协作平台。”Anthropic 用三个要点列出了 Prove2Me 的具体贡献：
“维护一个定理命题的有向无环图（DAG），智能体用它来决定下一步应该尝试哪些证明。这对于缓解记忆衰退和允许多个智能体并行工作特别有帮助。”
“通过将定理命题和证明分离到不同的文件中，并独立维护它们之间的链接，从而加快 Lean 的编译速度并最大程度地减少资源消耗。”
“通过为每个定理命题维护自然语言描述来支持搜索和复用，从而实现更简单的证明路径。”
请将这些视为存储库（store）的三个属性，而不仅仅是数学工具的三个功能。
第一点是具有依赖结构的外部化。已证明的内容以及每个结果所依赖的条件的记录存在于每个智能体之外。Anthropic 用来描述这一修复效果的词非常值得铭记：“缓解记忆衰退”。不是“协调工作”——而是缓解智能体所持记忆的衰退。
第二点是将主张与证据分离。命题放在一个地方，证明放在另一个地方，并且“它们之间的链接独立维护”。Anthropic 将其好处归结为编译速度和资源消耗，这确实没错。但对智能体而言，其结果是你可以阅读整套已确立的命题，而无需拖着庞大的证明主体。随着语料库增长超过 1300 万行，查阅索引的成本依然很低。
第三点是用于检索的通俗语言描述。每个定理命题都带有一个自然语言描述，其明确目的是“支持搜索和复用”。形式化命题非常精确，但极难搜索。而描述虽然不精确，但却易于查找。如果没有它，需要某个已存在结果的智能体将无法定位它，从而导致重复证明。
接下来这个细节最能说明其中哪一点最重要。Anthropic 运行了一个缩小版的实验：“Anthropic 的研究人员进行了一个小型实验，使用三个个人 Claude Max 订阅计划来形式化哈代-利特尔伍德圆法（Hardy-Littlewood Circle Method）的应用。完全通过 Prove2Me 进行协作，这些智能体在短短三天内就共同完成了维诺格拉多夫三素数定理（Vinogradov's Three Primes Theorem）的形式化。”他们的结论是：“我们认为，有了合适的脚手架，使用消费级 AI 订阅来协作形式化重大成果是可行的。”
三个消费级订阅和相同的脚手架在三天内就产生了一个著名的定理。这个脚手架承担了大量的工作。
这改变了什么，又没有改变什么
这并不表明智能体需要外部记忆才能具备强大的能力。这些智能体极其能干，即使在失败的尝试中也是如此——Anthropic 指出，它们未成功的尝试仍然在最终证明的非模板代码行中占了很大比例。能力从来都不是瓶颈。
它确实展示了在大规模运行下什么会最先崩溃，而那并不是推理能力。而是“知道什么是已知的真实情况”。Prove2Me 的这三个特性每一个都围绕着这个问题：什么已被确立、它依赖于什么，以及我能否找到它。当一次运行有数十个参与者和三万个已确立的结果时，“我们已经知道了什么”就成了最主要的成本，而且没有一个参与者能够独自记住答案。
这并不意味着上下文窗口无关紧要。更大的窗口可以帮助单个智能体在每次会话中做更多的事情。但它也无法扩展到这种程度：1300 万行 Lean 代码和 30,300 个已证明的定理，在任何合理的尺寸下都不是上下文窗口能解决的问题，更重要的是，它们不是一个检索解决方案——将材料放在窗口中并不等同于知道哪一部分能解决你当前的问题。这种区别正是为什么长上下文不是记忆中的核心论点。
这也不意味着这可以推广到关于所有智能体记忆的结论。形式数学对于共享记录来说是一个异常友好的领域：命题是明确的，依赖关系是显式的，并且有检查器来判定真伪。而你的代码库不具备这些属性。可以迁移的不是 DAG，而是这三个在任何地方都适用的特性。
人们会从中得出什么结论（以及为什么不应该得出这些结论）
“它就是一个待办事项列表。” DAG 是回答“下一步做什么”的部分，也是这三个特性中最难迁移的。你的工作无法分解为可证明命题的依赖图。可迁移的部分是主张与证据的分离以及通俗语言描述，这两者都关乎寻找已解决的问题，而不是分配工作。
“所以我们需要一个图数据库。” 不。图之所以存在，是因为定理的依赖关系确实是一个图。你真正需要的是一个查询成本低且可搜索的已确立结论记录。数据结构应取决于你的业务领域。
“现在消费级订阅计划就足够了。” Anthropic 的说法更为狭隘且有所保留：有了合适的脚手架，协作形式化“是可行的”。这一论断指的是脚手架的杠杆作用，而不是说不同级别的订阅计划可以互换。
“Claude 存在记忆问题。” 这是对一家公司公布自身失败尝试的错误解读。Anthropic 在其产品中记录了记忆功能，而这次运行在自定义测试框架中使用了内部研究模型。准确的说法是架构层面的，且适用于每个厂商：数十个并行智能体在同一个项目上工作 11 天，无法共同持有一个不断增长的已确立事实的共享记录，而解决方法是将该记录置于所有智能体之外。Anthropic 愿意公布这一失败，才使得这一发现具有实用价值。
解决方案：构建具有这三个特性的记录，而不是图
步骤 1：写下结论，并将其与产生这些结论的工作分离开来
对于普通项目而言，Prove2Me 最重要的举措是将命题与证明分离，“并独立维护它们之间的链接”。在工程上的等价做法是：将结论保存在一个地方，而将证据保留在它原本所在的地方。
结论只有一句话。“对账任务绝不能使用批量端点（batch endpoint）。”证据则是故障工单、拉取请求（PR）或你们解决该问题时的讨论帖。不要将证据复制到记录中——而是提供链接。需要了解约束条件的智能体只需阅读一句话。需要了解原因的智能体只需阅读一句话，然后点击链接。
这是保持记录在增长过程中依然可用的纪律。常见的失败恰恰相反：存储库中充斥着会议记录和长篇文档，要找到确定的答案意味着必须重新阅读整个论证过程。那只是一个归档库，而包罗万象的归档库解决不了任何问题。
步骤 2：为每个条目提供一个通俗语言描述，以便于你实际进行的搜索
Prove2Me 专门为每个定理命题附加了自然语言描述，以支持“搜索和复用”。形式化命题本来就在那里，但它是不可查找的。
你的同类问题更严重，因为你的结论本来就是散文体（prose），你会以为这使得它们是可搜索的。但如果这些文字使用的是你写作当天的词汇，那就并非如此。一个标题为“流式解析器决策”的记录条目，在六个月后，不会被一个正在解决摄取路径中记忆退化问题的智能体找到。
用人们寻找它时会使用的词汇来编写描述，包括故障现象。“摄取路径使用流式解析器，而不是批量加载器，因为批量加载器会将整个负载保存在内存中，并在大文件上传时导致 OOM 重启。”这读起来有些冗余，但这恰恰是让它可检索的原因。
步骤 3：将其放在所有参与者都能阅读同一副本的地方
失败的尝试之所以失败，是因为每个智能体都在维护自己的画像。一个共享的外部记录才是解决之道——而且“共享”必须包括你稍后加入的参与者以及人类。
实际上，这意味着一个可以通过协议访问的存储库，而不是嵌入在某一个工具中。如果记录保存在一个仓库的文件夹中，那么下一个服务中的智能体就无法看到它。如果它保存在某个编辑器的本地存储中，你的队友也无法看到。这两种情况都会导致一份优秀的记录悄然变成个人记录，这也是我们在Claude Code 智能体团队与上下文中探讨过的失败模式。
在 MemoryLake 中进行设置
MemoryLake 是一个围绕这三个特性构建的存储库：结论与背后的材料分开保存、为检索而非归档而描述，并且项目中的每个智能体和人员都可以通过同一个接口进行读取。它不是一个证明助手，也不进行形式化验证；它是 Anthropic 运行中不可或缺的那一层的普通工作版本。
步骤 1：创建 API 密钥
生成密钥并在大约 30 秒内发出你的第一次请求。一个密钥就能让“每个参与者阅读同一个副本”成为现实，而不仅仅是美好愿景。
步骤 2：上传你的第一批记忆
放入已经包含你确定结论的文档、图像和文件——事后分析、架构决策记录、每个人都会引用的设计评审。然后添加这些文档实际确立的一句话结论，这样无需阅读长篇大论即可检索到简短版本。
步骤 3：连接你的 AI 和智能体
让 Claude、Codex、OpenClaw 和其他智能体通过 MCP 或 API 进行访问。在任务开始时读取，在做出决策时写回结论，记录就能保持最新，而无需任何人专门安排文档整理日。
这在实践中改变了什么
并行智能体不再重复工作。这正是 Anthropic 报告的确切好处——DAG “允许了多个智能体并行工作”——而且这不需要图。它只需要一个即将解决某事的智能体能够发现该问题已被解决。
长期项目不再退化。“记忆衰退”是对任何重度依赖智能体的项目在第三周发生的情况的极佳描述：共享的理解变得稀薄，同样的问题在信息更差的情况下被重新争论。外部记录并不能解决所有问题，但它消除了“没人能说清决定了什么”这类问题。
模型更换不再意味着重置。FLT 运行在自定义测试框架中使用了单个内部模型；而你的项目每年会更换几次模型。当记录是外部的时，更换模型只会影响速度和成本，而不会影响积累的知识。
并且增加参与者的成本降低了。Anthropic 的三个订阅实验是文中对此最强有力的证据：脚手架使一个小型配置在解决严肃问题时变得富有成效。一个新工程师或新智能体加入一个拥有真实记录的项目，在第一天就能开展工作，而不是花一个月的时间来吸收上下文。
长期智能体项目中共享记录的最佳实践
每个结论一句话。 如果需要一个段落，那么该段落就是证据，应该放在链接后面。
务必附带原因。 没有原因的结论只是一条规则，而规则会被推翻。Anthropic 的智能体需要依赖关系也是出于同样的原因：一个你无法证明其合理性的结果，是一个你无法安全地在其基础上进行构建的结果。
为以后要运行的搜索进行描述。 包含故障现象和问题的词汇，而不是你解决问题当天的词汇。
明确记录更替情况。 当决策发生逆转时，说明情况和时间。一个默默丢弃旧版本的记录无法解释新版本。
将其保留在任何单个仓库或编辑器之外。 一旦它成为某个地方的本地内容，它就不再是共享的了，而共享正是整个解决方案的核心。
结论
头条成果是一个数学成果，它理应受到关注：首个完整的、经计算机验证的费马大定理证明，在 11 天内产生，并由 Lean 根据 Mathlib 自身的定理命题进行了验证。Anthropic 摘录的 Claude 在成功那一刻的想法——“FLT 根节点在 prove2me 上显示为已证明（PROVED）”——读起来令人瞩目。
运营层面的结果则更小、更具移植性。首次尝试失败是因为数十个智能体“很快就失去了对项目状态的追踪”，而解决这一问题的是一个置于它们所有人之外、具有三个特性的记录：依赖结构，以便结果可以建立在结果之上；主张与背后的证据分开存储，以便记录的读取成本保持低廉；以及每个条目上的通俗语言描述，以便任何已确立的事实都能被再次找到。随后，在三个消费级订阅上运行的相同脚手架在三天内就产生了另一个著名的定理。
这些都与数学无关。它关乎这样一个事实：在任何有多个参与者的长期项目中，瓶颈不再是能力，而是知道什么是已知的真实情况。Anthropic 的运行需要一个地方来记录这一点。你的项目同样需要。