Hacker News Reader

> We'll know that the time draws nearer when an AI confirms or refutes Mochizuki's proof of the abc conjecture. As of right now, I don't think they're capable of doing that. And, as they can't even check a very (very!) complex proof, they won't be able to conjure any inhumanly complex proofs de novo.

I agree, but... Spend time formalising a large part of existing mathematics and proofs, train a bunch of sufficiently powerful and generative models with that, and with cooperative problem solving and proof strategies, and give them access to proof assistants and adequate compute resources, and something interesting could happen.

I suspect the barrier is finding a business model that would pay for this. Turning mathematics into an industrial, extruded-on-demand product might work, but I dont know who (except maybe the NSA) would stump-up the money.

I am not suggesting models will be capable of generating 'all' proofs - that is clearly impossible. Merely that they will get better at doing so, and there is no clear reason at the moment to believe they will never reach a human level of competence. If you have one model functioning at such a level, it is presumably trivial to have a million of them, none of which will need to be paid, housed, or sleep etc.

Why would an AI confirmation or rejection be more convincing than the proof itself?

Rejection: an incredibly complex proof can fall for (comparatively) simple reasons. If the AI scans the entire proof and says yep, there's the flaw, page 126 theorem X contradicts <well established known theorem> then a human can verify this without having to understand the whole proof.

This could lead to the proof being rejected entirely, or fixed and strengthened.

Confirmation: if the AI understands it well enough that we're even considering asking it to confirm the proof, then you can do all kinds of things. You can ask it to simplify the entire proof to make it easier for humans to verify. You can ask it questions about parts of the proof you don't understand. You can ask it if there's any interesting corollaries or applications in other fields. Maybe you can even ask it to rewrite the whole thing in LEAN (although, like the author, I know nothing about LEAN and have no idea if this would be useful).

Presumably an AI would formalise the proof in a system such as Lean, then you only need to trust the kernel of that proof system.

Rejecting a proof would be more complicated, because while for confirming a proof you only need to check that the main statement in the formalisation matches that of the conjecture, showing that a proof has been rejected requires knowledge of the proof itself (in general).

> requires knowledge of the proof itself (in general)

Why? If a proof is wrong it has to be locally invalid, i.e. draw some inference which is invalid according to rules of logic. Of course the antecedent could have been defined pages earlier, but in and of itself the error must be local, right?

Human-written proofs are not written in Lean to be checked easily and there'll be potentially many formalizations for written prose and only some of them will be what the author intended. You need to pick the right formalization before you can say that this proof has local errors.

If a human reviewer rejects a proof, what do they consider apart from local errors? Formal proofs have formal local errors (which can be checked mechanically), while informal proofs have informal local errors (which require humans and some degree of hermeneutics to check). Am I missing something?

It might be using some nonlocal context e.g. something similar was proved earlier in the proof and the reader is assumed to remember and/or generalize this or there's some assumptions that are stated only in the beginning. There's also probably a bit of skipped proofs of the kind "I'll be able to do this if pressed, but so will the reviewer".

also why would capitalists expand resources on churning out proof after proof when mathematical proofs are not patentable?

That will change quickly if capitalists see that as an obstacle. Right now, they don't really care about that, as for example software (much of which is just math) is already patentable in the US.

A reasonable question - another way of looking at it is that theorems are just a side effect of mathematical research. Much of the world economy depends on things like cryptography, which involves a bunch of theorems. The question is then 'what as yet undiscovered mathematical realms might models think up that could make people money'? It is hard to imagine what doesn't exist yet, but much harder to imagine that all potentially profitable mathematics has already been discovered. This could 'just' look like algorithmic improvements.