4 ms·

TheoremDB – A public workspace for machine mathematics

104 points by frozenseven 2mo ago

vouaobrasil 2mo ago
I 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.
- Hackbraten 2mo ago
  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.
  - woopsn 2mo ago
    A proof may be impossible to fully grok, since about Leibniz - but problems will be solved now without even understanding the problem statement.
  - vouaobrasil 2mo ago
    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.
    - dolia 2mo ago
      This applies to a lot of scientific and practical (like construction) topics in general. Everyone relies on someone else (or something else) knowing what to do.
amitport 2mo ago
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.
- whattheheckheck 2mo ago
  https://github.com/math-inc/OpenGauss https://github.com/math-inc/OpenGauss https://www.math.inc/vision https://www.math.inc/vision Just use lean
- philipfweiss 2mo ago
  (Project creator here): 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.
butokai 2mo ago
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/ https://math.andrej.com/2026/07/11/making-ai-smarter-with-ai...
- vatsachak 2mo ago
  Is there any advantage of this over an agent using a Google search? 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.
realsarm 2mo ago
Wasn't using a source-grounded AI with citations a better natural choice than chatgpt with hallucinations?
igorkraw 2mo ago
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
empath75 2mo ago
Love the idea, but the website is just broken.. problem statements don't load, etc..
- vatsachak 2mo ago
  Vibe coded
- philipfweiss 2mo ago
  (Project creator here): Someone actually posted the site without me- I wasn’t planning on launching for a few weeks! If you see any issues, feel free to report them and i’ll get on fixing them right away! I’m active on the discord, feel free to report any bugs there. https://discord.gg/ds23BgPq6 https://discord.gg/ds23BgPq6
vatsachak 2mo ago
Why do LLM coded websites seem so obvious? Like an earnest project in this direction would probably look like a 90s html page
- timmg 2mo ago
  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?
  - vatsachak 2mo ago
    Did you try using the website? It's broken lol
    - lagrange77 2mo ago
      Yeah, interestingly it feels equally bland as the 90s pendants.
philipfweiss 2mo ago
Project creator here- I really did not expect it to get posted on hackernews! A nice surprise for sure though. Seems 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 https://discord.gg/ds23BgPq6
tidepooler 2mo ago
[flagged]

104 points by frozenseven 2mo ago

I 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.

Hackbraten 2mo ago
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.
- woopsn 2mo ago
  A proof may be impossible to fully grok, since about Leibniz - but problems will be solved now without even understanding the problem statement.
- vouaobrasil 2mo ago
  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.
  - dolia 2mo ago
    This applies to a lot of scientific and practical (like construction) topics in general. Everyone relies on someone else (or something else) knowing what to do.

amitport 2mo ago

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.

whattheheckheck 2mo ago
https://github.com/math-inc/OpenGauss https://github.com/math-inc/OpenGauss https://www.math.inc/vision https://www.math.inc/vision Just use lean
philipfweiss 2mo ago
(Project creator here): 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.

butokai 2mo ago

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/ https://math.andrej.com/2026/07/11/making-ai-smarter-with-ai...

vatsachak 2mo ago
Is there any advantage of this over an agent using a Google search? 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.

realsarm 2mo ago

Wasn't using a source-grounded AI with citations a better natural choice than chatgpt with hallucinations?

igorkraw 2mo ago

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

empath75 2mo ago

Love the idea, but the website is just broken.. problem statements don't load, etc..

vatsachak 2mo ago
Vibe coded
philipfweiss 2mo ago
(Project creator here): Someone actually posted the site without me- I wasn’t planning on launching for a few weeks! If you see any issues, feel free to report them and i’ll get on fixing them right away! I’m active on the discord, feel free to report any bugs there. https://discord.gg/ds23BgPq6 https://discord.gg/ds23BgPq6

vatsachak 2mo ago

Why do LLM coded websites seem so obvious? Like an earnest project in this direction would probably look like a 90s html page

timmg 2mo ago
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?
- vatsachak 2mo ago
  Did you try using the website? It's broken lol
  - lagrange77 2mo ago
    Yeah, interestingly it feels equally bland as the 90s pendants.

philipfweiss 2mo ago

Project creator here- I really did not expect it to get posted on hackernews! A nice surprise for sure though. Seems 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 https://discord.gg/ds23BgPq6

tidepooler 2mo ago

[flagged]