nybsjytm

8 ms·

1.
by nybsjytm 1y ago
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. Moreover
2.
by nybsjytm 1y ago
> 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 which is close eno
3.
by nybsjytm 1y ago
> 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 even part o
4.
by nybsjytm 1y ago
> 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 approach and coul
5.
by nybsjytm 1y ago
> 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 fluid mechan
6.
by nybsjytm 1y ago
Not sure what this has to do with my post.
7.
by nybsjytm 1y ago
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 which GPT impr
8.
by nybsjytm 2y ago
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
9.
by nybsjytm 2y ago
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 self-presents
10.
by nybsjytm 2y ago
> 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 famous except
11.
by nybsjytm 2y ago
> 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 a major cave
12.
by nybsjytm 2y ago
I consider it unconfirmed until it happens! No idea where I saw it but it was probably on twitter.
13.
by nybsjytm 2y ago
This takes for granted a formal setting, which is what I'm questioning in any of these 'real world' contexts.
14.
by nybsjytm 2y ago
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 desc
15.
by nybsjytm 2y ago
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
16.
by nybsjytm 2y ago
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 the tradeoff
17.
by nybsjytm 2y ago
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 l
18.
by nybsjytm 2y ago
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.
19.
by nybsjytm 2y ago
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 chatbot like ChatGPT
20.
by nybsjytm 2y ago
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 confidence that m
21.
by nybsjytm 2y ago
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 a formal language!)
22.
by nybsjytm 2y ago
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.
23.
by nybsjytm 2y ago
> 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 the answer wrong. Wh
24.
by nybsjytm 2y ago
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, isn't very
25.
by nybsjytm 2y ago
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 since you just ha
26.
by nybsjytm 2y ago
There are some AI guys like Christian Szegedy who predict that AI will be a "superhuman mathematician," solving problems like the Riemann hypothesis, by the end of 2026. I don't take it very seriously, but that kind of progno
27.
by nybsjytm 2y ago
This has to come with an asterisk, which is that participants had approximately 90 minutes to work on each problem while AlphaProof computed for three days for each of the ones it solved. Looking at this problem specifically, I think that m
28.
by nybsjytm 2y ago
Why have they still not released a paper aside from a press release? I have to admit I still don't know how auspicious it is that running google hardware for three days apiece was able to find half-page long solutions, given that the p
29.
by nybsjytm 2y ago
Hinton was never in the running for a Fields medal since he never made a single contribution to the field of mathematics. His work is about empirical discoveries in CS.
30.
by nybsjytm 2y ago
An incomprehensibly silly publicity stunt!

More ›