Love the idea, but the website is just broken.. problem statements don't load, etc..
TheoremDB – A public workspace for machine mathematics
11–20 of 22 posts
Re: TheoremDB – A public workspace for machine mathematics
#12Andrej 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...
I feel like the main benefit of such an endeavor would be to create a centralized database of mathematical theorems. But why aren't we using Lean theorems as the nodes instead?
The holy grail would be constructing an encoder that takes in a lean theorem and produces a meaningful latent vector so that whatever future math AI can instantly look up previously used "tricks" as opposed to only theorems.
I've met Andrej and he's obviously a genius so I'm sure this is useful.
Re: TheoremDB – A public workspace for machine mathematics
#13Like an earnest project in this direction would probably look like a 90s html page
Re: TheoremDB – A public workspace for machine mathematics
#14Why do LLM coded websites seem so obvious? Like an earnest project in this direction would probably look like a 90s html page
If you wanted to build a website right now, why would you hand-code an ugly version when you could get an LLM to do it quickly, cheaply and have it much better looking?
Re: TheoremDB – A public workspace for machine mathematics
#15Why do LLM coded websites seem so obvious? Like an earnest project in this direction would probably look like a 90s html page
Why? If you wanted to build a website right now, why would you hand-code an ugly version when you could get an LLM to do it quickly, cheaply and have it much better looking?
Re: TheoremDB – A public workspace for machine mathematics
#16Earlier quoted context omitted.
Why? If you wanted to build a website right now, why would you hand-code an ugly version when you could get an LLM to do it quickly, cheaply and have it much better looking?
Did you try using the website? It's broken lol
Re: TheoremDB – A public workspace for machine mathematics
#17I'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.
Re: TheoremDB – A public workspace for machine mathematics
#18Seems like someone found the site and posted without me.
I am still working on the site and was planning on launching in a few weeks. There are some usability issues and some features on my roadmap I haven’t gotten to yet.
That said- if folks are interested in helping contributing new problems/proofs, hunting bugs, or giving suggestions, we have a discord https://discord.gg/ds23BgPq6
Re: TheoremDB – A public workspace for machine mathematics
#19I'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.
I have 0 interest in commercializing this.
Im taking a lot of inspiration from MathOverflow, where I’ve been a user for several years. I think there is a protocol approach to this project that can be built, but it’s not what I’m building. I’m optimizing more for building in community features, since that is the genre of site I have enjoyed using in the past.
Re: TheoremDB – A public workspace for machine mathematics
#20Love the idea, but the website is just broken.. problem statements don't load, etc..
I’m active on the discord, feel free to report any bugs there. https://discord.gg/ds23BgPq6