4 ms·
Of course one of the first things that come to mind when reading the title is first having some sort of AlphaGo-style AI go wild on collections of math proofs a
by t_mann 4y ago
Of course one of the first things that come to mind when reading the title is first having some sort of AlphaGo-style AI go wild on collections of math proofs and then maybe some AlphaZero-style model that can get to work even without the library.
But I guess a fundamental problem for an RL-based approach (and a pretty interesting question in itself) is how difficult it would be to say what makes any mathematics "interesting".
The interview touches on the Langlands program several times, and that is a good example: how "interesting" Fargues-Fontaine curves were perceived (even by their creators) changed substantially after Peter Scholze created a whole new world for that curve to live in. So how do we tell the computer that they're sort of halfway to something really interesting, and, perhaps even more importantly, how do we communicate it to humans once we're there? Even Scholze himself was skeptical when first presented with this direction, and those are the humans most intimately familiar with those theories. Imagine how hard it would be for any human to grasp what the AI had just done, let alone judge its relevance, after it's made progress on its own, using new mathematical objects it had just developed, solving problems it had set itself. It's not like DALL-E, where anyone can just go and say - yeah, that looks like a cat with a party hat, great job.
- Jimmy 4y agoNaturally, the first step for AI mathematics would be generating proofs of theorems that humans have already deemed interesting, rather than the AI generating entirely new research directions all by itself. Certainly it’s an interesting problem to think about how one would formalize the notion of interesting/important mathematics. But it’s not necessary to solve that problem in order for AI to start having a big impact on how mathematics is done.
- IIAOPSW 4y agoThis implies that the discovery of math and the existence of math ultimately comes down to human taste and can only be learned by studying humans. I'd like to think human reasoning is a crude approximation to mathematics in all its glorious purity, not the other way around.
- 323 4y agoBig results typically have a lot of implications and connect different fields together. This sounds like something that could be measured objectively. You can also try reproving old theorems with newly discovered methods. So if suddenly you can reprove results in different fields with a new method, that sounds like something that might be big and should be investigated by humans. Of course, what I wrote above will miss subtle things, but there is a place for a system which can just brute force it's way through mathematics.