[xg15]

Ah, thanks for the clarification. Then the whole thing makes a lot more sense - though I'd say the outlook also becomes more optimistic.

I thought the rhetoric sounded somewhat like the AGI/accelerationist folks who postulate some sort of eventual "godlike" AI whose thought processes are somehow fundamentally inaccessible to humans. So if you had a proof that was only understandable to this sort if AIs, then mathematics as a discipline of understanding would be over for good.

But this sounds like it would at least theoretically let you tackle the proof? Like, it's imaginable that some AI generates a proof that is several TB (or EB) in size but still validates - which would of course be impossible to understand for human readers in the way you can understand a paper. But then "understanding" that proof would probably become a field of research of its own, sort of like the "BERTology" papers that try to understand the semantics of specific hidden states in BERT (or similar approaches for GPTs).

So I'd see an incomprehensible AI-generated proof not as the end of research in some conjecture, but more as a sort of guidance: Unlike before, you now know that the treasure chest exist and you even have its coordinates, you just don't have the route to that location. The task then becomes about figuring out that route.

[oersted]

In terms of having the proofs be understandable to humans, I'd say that's still a challenge. Not a fundamental challenge, but a real practical challenge still.

Lean makes the proofs verifiable, and sure to a degree understandable, but normal Lean proofs written by humans are already a challenge to understand without additional documentation, and, as with all code-generation, AI generated proofs are probably even harder to understand. There are many paths to arrive at a proof, the AI may take very messy routes that don't align with how humans create abstractions and assign meaning to break the process down into understandable steps.

In a sense all AI is understandable, nothing is hidden, you can see all the numbers inside a Transformer. Just being able to see the code might not necessarily help mathematicians too much in extracting deeper meaning and lessons from AI-generated proofs, at least not without significant additional work.

[oersted]

There's an argument to be made that incomprehensible proofs are still very useful.

I understand that mathematicians are all about understanding why a theorem is true, not just checking that it is, and then using that understanding to push forward other research. Same as most scientists care more about understanding how the world works rather than developing methods to control and manipulate it.

But proven theorems are mathematical tools that can be used to make progress, regardless of your understanding of how they work. I think there is a path forward for maths as an engineering discipline, possibly with much faster progress, just as computer science expanded into software engineering. AI is just the next step of many, software libraries, interfaces and abstractions are also black-boxes in a sense that do stuff for you without knowing how.

A good engineer learns to build on the shoulders of giants, mastering the understanding of what tools do and how they behave, without necessarily needing to know how they are built from scratch. It might be less satisfying to the curious, but you can get a lot more done.

[nicf]

Incomprehensible proofs are indeed still useful to some extent, and I don't think you'll find many mathematicians who would reject them as an answer to the binary question of whether the result is true.

But when you talk about "getting a lot more done," I want to ask, get a lot more done to what end? Despite what mathematicians sometimes write in their grant applications, resolving most of the big open problems in the field probably won't lead to new technologies or anything. To use the Riemann Hypothesis example again, most number theorists already think it's probably true, and there are a lot of papers being published already which prove things like "if the Generalized Riemann Hypothesis is true, then [my new result]".

No one is really waiting around just for the literal, one-bit answer to the question of whether RH is true; if we got that information and nothing else, I'm sure number theorists would be happy to know, but not a whole lot about the work being done in the field would change. It's not just being "satisfying to the curious"; virtually the entire reason we want a proof is to use the new ideas it would presumably contain to do more mathematics. This is exactly what's happened with the proof of the Poincare Conjecture, the only one of the Millennium Problems that's been resolved so far.

This is what I was lamenting in my comment earlier: the thing you're describing, where we set proof-finding models to work and they spit out verifiable but totally opaque proofs of big open problems in math, very well might happen someday, but it wouldn't actually be all that useful for anything, and it would also mean the end of the only thing about the whole enterprise that the people working in it actually care about.

[xg15]

Yeah, I imagine in those situations, an AI proof that the conjecture is false would probably be more interesting and useful than a proof that it is true.

A proof of the conjecture would essentially just move the situation from "we think there could be counterexamples, but so far we haven't found any" to "there really are no counterexamples anywhere, you can stop looking". The interesting thing here would be the explanation why there can be no counterexamples, which is exactly the thing that the proof wouldn't give you.

On the other hand, a counterproof would either directly present the community with a counterexample - and maybe reveal some interesting class of objects that was overlooked so far - or at least establish that there have to be counterexamples somewhere, which would probably give more motivation to efforts of finding one.

(Generally speaking here. I'm not a mathematician and I can't really say anything about the hypotheses in question)

[nicf]

Yeah, that's definitely right --- an explicit counterexample to the Riemann Hypothesis would be very surprising and interesting, and I think that would be equally true no matter whether it was found by a person or a computer! The situation that would be mostly unhelpful is a certificate that the result is true that communicates nothing about why.