I called it the easiest part of his papers, not easy. Either way, it's actually not relevant to the proof. For example, I believe that Morgan and Tian's 500 page exposition of the proof doesn't mention it even once.…
> brilliantly realised Can you say more about this? Nothing about this approach seems very amazing to me. Construct an approximate solution by some numerical method (in this case neural networks), prove that a solution…
> Folks knew the problem was near a solution once the monotonicity proof of the W functional came out. This isn't true, it was a major accomplishment but by far the easiest part of Perelman's papers and not actually…
> PINNs are different in concept, yes, but clearly no less important If anything I think they're more important! Whether or not it works out for Navier-Stokes, this kind of thing is an extremely plausible avenue of…
> I know they are so close to a computationally-assisted proof of counterexample that it is virtually inevitable at this point. That's a strong claim. Is it based on more than the linked work on some model problems from…
Not sure what this has to do with my post.
Any mathematicians who have actually called it "new interesting mathematics", or just an OpenAI employee? The paper in question is an arxiv preprint whose first author seems to be an undergraduate. The theorem in it…
There's a related section about 'mathiness' in section 3.3 of the article "Troubling Trends in Machine Learning Scholarship" https://arxiv.org/abs/1807.03341. I would say the situation has only gotten worse since that…
Much physicist math can't be made rigorous so easily! Which isn't to say that much of it doesn't still have great value. However the math in AI papers is indeed different. For example, Kingma and Ba's paper…
> Checking the correctness of proofs is a much easier problem than coming up with the proof in the first place. Just so this isn't misunderstood, not so much cutting-edge math is presently possible to code in lean. The…
> Many AI researchers are mathematicians. Any theoretical AI research paper will typically be filled with eye-wateringly dense math. AI dissolves into math the closer you inspect it. It's math all the way down. There is…
I consider it unconfirmed until it happens! No idea where I saw it but it was probably on twitter.
This takes for granted a formal setting, which is what I'm questioning in any of these 'real world' contexts.
Hmmm I think even in something very nominally nearby like theoretical physics, there's very little that's similar to theorem proving. I don't see how AlphaProof could be a stepping stone to anything like what you're…
You don't even need AI to regurgitate Perelman's papers, you can do that in three lines of python. What I meant is that there's no AI you can ask to explain the details of Perelman's proof. For example, if there's a…
Very plausible, but that would also be noteworthy. As I've mentioned in some other comments here, (as far as I know) we outside of DeepMind don't know anything about the computing power required to run alphaproof, and…
If this were the case, I don't see why we'd need to wait for an AI company to make a breakthrough in math research. The key issue instead is how to encode 'real-life' statements in a formal language - which to me seems…
The quality of AI algorithms is not based on formal mathematics at all. (For example, I'm unaware of even one theorem relevant to going from GPT-1 to GPT-4.) Possibly in the future it'll be otherwise though.
No, nobody has proved it. Side point, there is no existing AI which can prove - for example - the Poincaré conjecture, even though that has already been proved. The details of the proof are far too dense for any present…
As a mathematician, of course I agree. But in a sentence like: > A speedup in the movement of the maths frontier would be worth many power stations who is it 'worth' it to? And to what end? I can say with some…
Being logical in social life is pretty much completely different from being logical in a mathematical argument, especially in a formal theorem proving environment. (Just try to write any kind of cultural proposition in…
It's worth emphasizing that it's been possible for years to use an automatic theorem prover to prove novel results. The whole problem is to get novel interesting results.
> A better question is what can happen when everybody has access to above average reasoning. Our society is structured around avoiding confronting people with difficult questions, except when they are intended to get…
For some time a 'superhuman math AI' could be useful for company advertising and getting the attention of VCs. But eventually it would be pretty clear that innovative math research, with vanishingly few exceptions,…
I agree that the result is important regardless. But the tradeoff of computing time/cost with problem complexity is hugely important to think about. Finding a proof in a formal language is trivially solvable in theory…
I called it the easiest part of his papers, not easy. Either way, it's actually not relevant to the proof. For example, I believe that Morgan and Tian's 500 page exposition of the proof doesn't mention it even once.…
> brilliantly realised Can you say more about this? Nothing about this approach seems very amazing to me. Construct an approximate solution by some numerical method (in this case neural networks), prove that a solution…
> Folks knew the problem was near a solution once the monotonicity proof of the W functional came out. This isn't true, it was a major accomplishment but by far the easiest part of Perelman's papers and not actually…
> PINNs are different in concept, yes, but clearly no less important If anything I think they're more important! Whether or not it works out for Navier-Stokes, this kind of thing is an extremely plausible avenue of…
> I know they are so close to a computationally-assisted proof of counterexample that it is virtually inevitable at this point. That's a strong claim. Is it based on more than the linked work on some model problems from…
Not sure what this has to do with my post.
Any mathematicians who have actually called it "new interesting mathematics", or just an OpenAI employee? The paper in question is an arxiv preprint whose first author seems to be an undergraduate. The theorem in it…
There's a related section about 'mathiness' in section 3.3 of the article "Troubling Trends in Machine Learning Scholarship" https://arxiv.org/abs/1807.03341. I would say the situation has only gotten worse since that…
Much physicist math can't be made rigorous so easily! Which isn't to say that much of it doesn't still have great value. However the math in AI papers is indeed different. For example, Kingma and Ba's paper…
> Checking the correctness of proofs is a much easier problem than coming up with the proof in the first place. Just so this isn't misunderstood, not so much cutting-edge math is presently possible to code in lean. The…
> Many AI researchers are mathematicians. Any theoretical AI research paper will typically be filled with eye-wateringly dense math. AI dissolves into math the closer you inspect it. It's math all the way down. There is…
I consider it unconfirmed until it happens! No idea where I saw it but it was probably on twitter.
This takes for granted a formal setting, which is what I'm questioning in any of these 'real world' contexts.
Hmmm I think even in something very nominally nearby like theoretical physics, there's very little that's similar to theorem proving. I don't see how AlphaProof could be a stepping stone to anything like what you're…
You don't even need AI to regurgitate Perelman's papers, you can do that in three lines of python. What I meant is that there's no AI you can ask to explain the details of Perelman's proof. For example, if there's a…
Very plausible, but that would also be noteworthy. As I've mentioned in some other comments here, (as far as I know) we outside of DeepMind don't know anything about the computing power required to run alphaproof, and…
If this were the case, I don't see why we'd need to wait for an AI company to make a breakthrough in math research. The key issue instead is how to encode 'real-life' statements in a formal language - which to me seems…
The quality of AI algorithms is not based on formal mathematics at all. (For example, I'm unaware of even one theorem relevant to going from GPT-1 to GPT-4.) Possibly in the future it'll be otherwise though.
No, nobody has proved it. Side point, there is no existing AI which can prove - for example - the Poincaré conjecture, even though that has already been proved. The details of the proof are far too dense for any present…
As a mathematician, of course I agree. But in a sentence like: > A speedup in the movement of the maths frontier would be worth many power stations who is it 'worth' it to? And to what end? I can say with some…
Being logical in social life is pretty much completely different from being logical in a mathematical argument, especially in a formal theorem proving environment. (Just try to write any kind of cultural proposition in…
It's worth emphasizing that it's been possible for years to use an automatic theorem prover to prove novel results. The whole problem is to get novel interesting results.
> A better question is what can happen when everybody has access to above average reasoning. Our society is structured around avoiding confronting people with difficult questions, except when they are intended to get…
For some time a 'superhuman math AI' could be useful for company advertising and getting the attention of VCs. But eventually it would be pretty clear that innovative math research, with vanishingly few exceptions,…
I agree that the result is important regardless. But the tradeoff of computing time/cost with problem complexity is hugely important to think about. Finding a proof in a formal language is trivially solvable in theory…