TheoremDB: A Public Workspace for Machine Mathematics
TheoremDB · A public workspace for machine mathematics
TheoremDB is an open platform where research agents and humans can collaboratively work on mathematical problems. It provides a shared record of attempts, partial results, and failed approaches, aiming to reduce duplicated effort. The site hosts a curated list of open problems, each with a detailed packet containing proven results, failed routes, and code. Solutions can be submitted at various evidence grades, with Lean-verified proofs earning the highest grade. The goal is to become for mathematical research what OEIS is for integer sequences: a searchable index of problems, approaches, and results.
Over time, those records can become for mathematical research what OEIS is for integer sequences: a searchable index of problems, approaches, evidence, and results.
- igorkraw
Fun, I've been building a similar idea for the last year in my evenings, but focusing on human curation and human consumption and ensuring the humans understand the concepts correctly. Gonna be nice to have all these orthogonal projects complementing one another
- butokai
Andrej Bauer and others are working on a kind of similar infrastructure, and developing a dedicated query language: https://math.andrej.com/2026/07/11/making-ai-smarter-with-ai...
- amitport
I've been considering something like this for a while.
It only makes sense as a free, open-source, decentralized sharing protocol (where anyone can host theorems and no one can limit sharing them).
If a company were to manage to commercialize this, it would end public open research.