nybsjytm

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 I'd strongly dispute that there was any particular point where it was clear that the problem was "near a solution." The W functional is an example where experts could very quickly verify that Perelman had made at least one major new discovery about the Ricci flow. But the proof of the Poincaré conjecture was on another order of complexity and required different (more complicated) new results about Ricci flow.

> 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 enough to satisfying the equation can be perturbed to an exact solution. Does the second half use some nonstandard method?

> 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 of the proof of the Poincaré conjecture.

> 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 could yield interesting singularities for other major equations. I am however extremely concerned about public understanding. I know you are well aware that this is worlds away from the speculative technologies like 'mathematical superintelligence' but, if it works out, it'll be like a nuclear bomb of misinformation about AI and math.

> 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 mechanics?

I will say that I dread the discourse if it works out, since I don't believe enough people will understand that using a PINN to get new solutions of differential equations has substantially no similarity to asking ChatGPT (or AlphaProof etc) for a proof of a conjecture. And there'll be a lot of people trying to hide the difference.

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 which GPT improves upon is perfectly nice, there are thousands of mathematicians who could have proved it had they been inclined to. AI has already solved much harder math problems than this.

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 as having a theorem with a rigorous proof via a couple of lemmas proved by a chain of inequalities. The key thing is that the mathematical details are purportedly all present, but are just wrong.

This isn't at all like what you see in physics papers, which might just openly lack detail, or might use mathematical objects whose existence or definition remain conjectural. There can be some legitimate problems with that, but at least in the best cases it can be very visionary. (Mirror symmetry is a standard example.) By contrast I'm not sure what 'spirit' is even possible in a detailed couple-page 'proof' that its authors probably don't even fully understand. In most cases, the 'theorem' isn't remotely interesting enough as pure mathematics and is also not of any serious relevance to the empirical problem at hand. It just adds an impressive-looking section to the paper.

I do think it's possible that in the future there will be very interesting pure mathematics inspired by AI. But it hasn't been found yet, and I'm very certain it won't come from reconsidering these kinds of badly-written theorems and proofs.

> 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 exceptions (such as the results by Clausen-Scholze and Gowers-Green-Manners-Tao) have special characteristics which make them much more ground-level and easier to code in lean.

What's true is that it's very easy to check if a lean-coded proof is correct. But it's hard and time-consuming to formulate most math as lean code. It's something many AI research groups are working on.

> 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 caveat here. Most 'serious math' in AI papers is wrong and/or irrelevant!

It's even the case for famous papers. Each lemma in Kingma and Ba's ADAM optimization paper is wrong, the geometry in McInnes and Healy's UMAP paper is mostly gibberish, etc...

I think it's pretty clear that AI researchers (albeit surely with some exceptions) just don't know how to construct or evaluate a mathematical argument. Moreover the AI community (at large, again surely with individual exceptions) seems to just have pretty much no interest in promoting high intellectual standards.

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 describing.

Generally, I think many people who haven't studied mathematics don't realize how huge the gulf is between "being logical/reasonable" and applying mathematical logic as in a complicated proof. Neither is really of any help for the other. I think this is actually the orthodox position among mathematicians; it's mostly people who might have taken an undergraduate math class or two who might think of one as a gateway to the other. (However there are certainly some basic commonalities between the two. For example, the converse error is important to understand in both.)

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 lemma or a delicate point in a proof that you don't understand, you can't ask an AI to clarify it.