TheoremDB – A public workspace for machine mathematics
1–10 of 21 posts
Re: TheoremDB – A public workspace for machine mathematics
#2I suspect tools like this will change human behaviour in the future so that no one really understands the math any more. If a solution to the Riemann hypothesis is found with it, I wouldn't be surprised if the person finding it didn't even understand analytic continuation. And that those that do just click like and scroll to the next problem.
Re: TheoremDB – A public workspace for machine mathematics
#3I'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
#4Andrej 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...
Re: TheoremDB – A public workspace for machine mathematics
#5I suspect tools like this will change human behaviour in the future so that no one really understands the math any more. If a solution to the Riemann hypothesis is found with it, I wouldn't be surprised if the person finding it didn't even understand analytic continuation. And that those that do just click like and scroll to the next problem.
Hasn’t this been the case for human-made proofs too?
For example, Andrew Wiles’s famous proof touched a number of different, barely-related mathematical fields that no single person could allegedly peer-review it on their own. That was in the 1990s.
Re: TheoremDB – A public workspace for machine mathematics
#6Wasn't using a source-grounded AI with citations a better natural choice than chatgpt with hallucinations?
Re: TheoremDB – A public workspace for machine mathematics
#7Fun, 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
Re: TheoremDB – A public workspace for machine mathematics
#8I suspect tools like this will change human behaviour in the future so that no one really understands the math any more. If a solution to the Riemann hypothesis is found with it, I wouldn't be surprised if the person finding it didn't even understand analytic continuation. And that those that do just click like and scroll to the next problem.
Hasn’t this been the case for human-made proofs too? For example, Andrew Wiles’s famous proof touched a number of different, barely-related mathematical fields that no single person could allegedly peer-review it on their own. That was in the 1990s.
A proof may be impossible to fully grok, since about Leibniz - but problems will be solved now without even understanding the problem statement.
Re: TheoremDB – A public workspace for machine mathematics
#9Love the idea, but the website is just broken.. problem statements don't load, etc..
Re: TheoremDB – A public workspace for machine mathematics
#10I suspect tools like this will change human behaviour in the future so that no one really understands the math any more. If a solution to the Riemann hypothesis is found with it, I wouldn't be surprised if the person finding it didn't even understand analytic continuation. And that those that do just click like and scroll to the next problem.
Hasn’t this been the case for human-made proofs too? For example, Andrew Wiles’s famous proof touched a number of different, barely-related mathematical fields that no single person could allegedly peer-review it on their own. That was in the 1990s.
No there were a few people that could. And in principle, if Andrew Wiles did it, others could too and were motivated to do it. What I'm saying is that people will be conditioned to explore less on their own with tools like this and thus fewer and fewer will bother understanding the proofs.
Math is getting very specialized it's true, and I think that's part of the motivation to use AI. The specialization is itself a bit of a problem, so AI is simultaneously exposing that and hiding it under another layer of abstraction.