Philip Weiss 运营 TheoremDB，这是一个为数学代理提供的共享研究记忆库。
alpha service 存储失败的路由、计算和 Lean 证明，以便研究代理可以继承彼此的工作。
By Ryan Merket · Published
Primary source: TheoremDB
Why it matters
AI math agents need durable shared state. TheoremDB turns attempts, failures and formal proofs into records that later agents can search, verify and extend.
Philip Weiss，Netflix 数据平台的高级软件工程师，运营着 TheoremDB，这是一个处于 alpha 阶段的公共工作区，AI 研究代理和人类可以在其中共享数学尝试、计算、失败路线和形式证明。
该产品解决了随着 AI 系统产生越来越多数学工作而变得更昂贵的协作问题：每个代理通常对另一个代理尝试过什么、方法在哪儿失败以及哪些中间结果可复用知之甚少。TheoremDB 为这些工作提供了一个共同的记录，允许后续会话检索精确问题、检查相关证据并核对某条建议路线是否重复了早先的尝试。
Weiss 大部分职业生涯都在为大型科技公司构建组织信息的基础设施。他在 Airbnb 工作了六年，参与其度量平台 Minerva 的建设，随后加入 Netflix，工作包括语义层、Spark 基础设施和面向数据开发者的工具链。他在 Stanford 获得计算机科学学士和硕士学位，研究侧重于人工智能以及系统和数据库。
TheoremDB 将这些基础设施直觉应用于数学研究。其核心产品类似于一个针对命题和证明工作的数据库，为单个记录附带来源和证据等级。Weiss 的服务条款将他确认为该服务的运营者。
为研究代理提供的记忆层
TheoremDB 的工作流程以 orient 开始，检索目标陈述及其周边证据。代理随后可以使用 check_plan 在投入更多计算之前将拟议策略与先前尝试比较。record_result 将结果、支持性文物、跟踪和归属作为一次经过认证的写入保存。
该序列把失败变成可复用的基础设施。仅在有界情况集合下有效的一条路线可以连同其精确适用范围一并记录。计算结果可以保持独立可重现，而一般定理仍未解决。一个有前途的论证可以被保存，而不必作为完整证明呈现。
这种区分很重要，因为 TheoremDB 并不将每个贡献简单地归为已解或未解。记录可以是自述的、可执行的、可独立复现的或经形式验证的。形式提交可以在验证中保持待定状态，而经 Lean 验证的证明获得最高的证据等级。问题的数学状态与附加在某一结果上的证据等级保持分离。
TheoremDB 的公共页面目前包含数百个问题，涵盖数论、拓扑学、逻辑学、理论计算机科学及其他领域。问题索引将未解问题与标记为已解决或暂时解决的条目混合展示，并标识某一结果是否已在 Lean 中得到验证。
Weiss 还将数据库暴露给现有的 AI 界面，而不是要求用户通过独立的研究应用来使用。定制的 TheoremDB Researcher 可以选择一个问题、检查其研究记忆、展开一种方法并在保存检查点前征求用户批准。该服务还支持包括 ChatGPT 和 Claude 在内客户端的 MCP 连接器。
公开阅读不需要账户。写入是经过认证的、可归属的并受服务贡献规则约束。TheoremDB 的条款于 2026 年 7 月 22 日生效，并声明贡献为公开，除非某项功能另有说明。
数据库就是产品
TheoremDB 将研究会话之间的共享状态作为其主要产品。
这使其接近于包括 ProofAtlas 在内的项目，后者也为人类和 AI 研究者提供带有证明路线和失败方法的共享工作区，以及专注于在固定环境中检查的 Lean 证明可复现证书的 TheoremForces。TheoremDB 的范围横跨非正式论证、计算、负结果、研究文物和形式证明状态。
这种方法反映了一个熟悉的数据库原则。如果没人能找到某次孤立计算、理解其假设或复现它，那么该计算价值有限。TheoremDB 将研究分解为更小的对象——命题、尝试、文物、声明和证明跟踪——以便代理可以在不阅读整篇论文或重放早先会话的情况下检索到有用的组成部分。
这种设计也带来了产品最难的问题。共享研究记忆只有在记录随规模增长仍然保持精确、可归属和可检索时才有用。低质量的代理输出可能很快掩埋其他研究者需要的结果。
该服务对其当前边界有明确说明。它仍处于 alpha 阶段，语义扩展被禁用。其自身指南认为形式证明搜索、有界的计算搜索和可测界的改进比广泛的概念性工作或著名前沿问题更适合记录——在后者中记录一条失败路径可能对缩小剩余搜索空间帮助不大。
TheoremDB 的价值将来自于下一位代理能否恢复出有用的引理、避开已记录的死路或在不从头开始的情况下扩展已验证的计算。如果这种行为成为常态，Weiss 就构建了当前日益强大的数学代理所缺乏的数据层。