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.
amitport 19 hours 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.
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
vatsachak 13 hours 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 11 hours 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 7 hours ago [-]
Did you try using the website? It's broken lol
lagrange77 4 hours ago [-]
Yeah, interestingly it feels equally bland as the 90s pendants.
realsarm 16 hours ago [-]
Wasn't using a source-grounded AI with citations a better natural choice than chatgpt with hallucinations?
vouaobrasil 20 hours 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 17 hours 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 15 hours 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 13 hours 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.
empath75 15 hours ago [-]
Love the idea, but the website is just broken.. problem statements don't load, etc..
vatsachak 13 hours ago [-]
Vibe coded
Rendered at 05:03:55 GMT+0000 (Coordinated Universal Time) with Vercel.
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.
If a company were to manage to commercialize this, it would end public open research.
https://www.math.inc/vision
Just use lean
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?
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.
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.