[explaininjs]

There’s always another encoding, all you prove is that there doesn’t exist a proof in the encoding you selected less than the length you specified, it does nothing at all to disprove the existence of a short proof in general.

[dellamonica]

Right, and this is also the current status of handmade mathematics. All we know is that we did not find a proof yet with everything that has been tried. This typically means that a problem is harder the more stuff has been thrown at it and failed.

A non deterministic Turing machine would absolutely crunch through math theorems, I really don't know why there is so much push back against what I am stating. Basically, if you had such a machine, there essentially would no longer be any room left for proving stuff the manual way, you would get completely outclassed by them.

The real consequence for me though is that this is a strong evidence (call it faith) against P=NP.

[explaininjs]

> A non deterministic Turing machine would absolutely crunch through math theorems

Can you formalize that statement in any useful way? It seems you believe proof validation to be in NP, when it most certainly is not. Accordingly an N-TM would be of relatively little power against the problem.

[dellamonica]

It's rather difficult to provide a good formalization but let me give it a shot.

Suppose that mathematicians write papers with pen and paper in a subset of natural language without ambiguity (you wish!). What they write as proofs can be checked thoroughly for correctness by some other human (referee) otherwise it will not be published (again, we wish!).

Now for a paper with N tokens (or chars or whatever measure of length) how much computation can the referee reasonably dedicate to the task of checking that proof. Unless you believe something special about the human brain, I'd claim that poly time on N is a reasonable assumption. Now this means that checking is poly(N) for human checkable proofs of length N.

This is my argument that non deterministic Turing machines would absolutely crunch through everything that we could do in the current model of mathemticsl research.

The class of instances is that of theorems which a human could write a hand made proof and have it verified by another human. Recall that we are discussing formalization and what AI could achieve in this space, so I think formulating what we currently can achieve is a nice contrast with what could come in the future.