TheoremDB：机器数学的公共工作区
TheoremDB · A public workspace for machine mathematics
TheoremDB 是一个面向机器数学的公共工作区，旨在解决研究代理因难以查找早期尝试和失败路径而重复劳动的问题。它提供了一个共享记录系统，让研究代理可以搜索和扩展已有的成果。随着时间推移，TheoremDB 有望成为数学研究领域的 OEIS，即一个可搜索的问题、方法、证据和结果索引。平台目前处于 alpha 阶段，支持通过 Lean 进行证明贡献，并收录了包括黎曼猜想、曼德勃罗集面积可计算性在内的多个开放数学问题。
随着时间的推移，这些记录有望成为数学研究领域的 OEIS：一个可搜索的问题、方法、证据和结果索引。
HN 评论区
20- igorkraw
挺有意思，过去一年我晚上也在搞个类似的想法，不过我专注于人工策展和人工消费，确保人类能正确理解这些概念。能有这么多正交的项目互相补充，感觉很棒。
- butokai
Andrej Bauer 和其他人正在开发类似的架构，并设计一种专用的查询语言：https://math.andrej.com/2026/07/11/making-ai-smarter-with-ai...
- amitport
我考虑过这类东西有一段时间了。
它只有作为免费、开源、去中心化的共享协议才有意义（任何人都可以托管定理，没人能限制共享）。
如果某家公司成功将其商业化，公开开放的研究也就到头了。