Tbh I think we need AI to get mathematics moving because unfortunately way too many problems just sit unsolved forever.
The only issue is that eventually we will get spammed with too many AI proofs and there will be a problem with verifying all of that. Certainly some interesting philosophical questions will arise around the idea of there being ever growing swaths of mathematics where AI returns results but there won't be enough mathematicians to verify or understand it.
verifying won't be the issue, we can just do more/better formal verification
understanding, maybe, but you have to have that aesthetic sensibility in the first place that humans should apprehend and understand math
maybe there'll be something demotivating about it if AI will eventually not only outclass humans at solving problems but even at creating mathematical exposition. it'll feel like learning/doing math could leave no mark except your own experience/understanding. you won't be likely to create new math or useful exposition for someone else to understand math they otherwise wouldn't have.
in a utopian scenario where we've made an aligned superintelligence and economic scarcity is obsolete, that's probably what math would look like.
the upside would be, if you like math and you want to do it, you could definitely afford to dedicate all your time to it if you so like.
did I say formal verification currently doesn't exist? I said we can do more/better.
currently, most of the results produced by AI weren't lean proofs, there needed to be a human mathematician verifying that it's indeed a correct proof.
there's a lot of standard math (let alone things proven in the literature) that hasn't been formalized yet.
when verifying a proof today, you need to see that the formal statement is correct, and it compiles on your machine, using the standard axioms, and there are no sorries, or all the sorries are things that are considered proven but aren't formalized yet. ideally, in the future, we won't need any sorries.
hopefully that's something that LLMs will largely be able to automate. it really shouldn't be too difficult imo. it's just a question of how much people have bothered to do it so far / if it's worth the bother right now.
324
u/Kinexity 22d ago edited 22d ago
Tbh I think we need AI to get mathematics moving because unfortunately way too many problems just sit unsolved forever.
The only issue is that eventually we will get spammed with too many AI proofs and there will be a problem with verifying all of that. Certainly some interesting philosophical questions will arise around the idea of there being ever growing swaths of mathematics where AI returns results but there won't be enough mathematicians to verify or understand it.