[dellamonica]

It doesn't require anything like that.

Math proofs are of NP complexity. If you had access to a non deterministic Turing machine you could enumerate all possible proofs of a given length and check them all in poly time.

That does not say anything about LLMs though. Personally, I believe they could be quite helpful to mathematicians in a way similar to copilot for software programming.

[Jweb_Guru]

> Math proofs are of NP complexity.

This is only true for very specific kinds of proofs, and doesn't apply to stuff that uses CiC like Lean 4. This is because many proof steps proceed by conversion, which can require running programs of extremely high complexity (much higher than exponential) in order to determine whether two terms are equal. If this weren't the case, it would be much much easier to prove things like termination of proof verification in CiC (which is considered a very difficult problem that requires appeal to large cardinal axioms!). There are formalisms where verifying each proof steps is much lower complexity, but these can be proven to have exponentially (or greater) longer proofs on some problems (whether these cases are relevant in practice is often debated, but I do think the amount of real mathematics that's been formalized in CiC-based provers suggests that the extra power can be useful).

[dellamonica]

This is all very interesting but it seems that we're just taking different views on what is the instance size. If it is the length of the theorem statement in some suitable encoding and the goal is to find a proof, of any possible length, then yeah, this is way too hard.

I'm taking the view that the (max) length of the proof can be taken as a parameter for the complexity because anything too long would not have any chance of being found by a human. It may also not be trusted by mathematicians anyway... do you know if the hardware is bug free, the compiler is 100% correct and no cosmic particle corrupted some part of your exponential length proof? It's a tough sell.

[zozbot234]

Yes, executing a calculation as part of a proof after separately proving that it is the "right" calculation to solve the problem is quite a common way of proceeding. Even common things like algebraic simplifications of all kinds (including solving equations, etc.) can be seen as instances of this, but this kind of thing has notably come up in the solution of famous problems like the 4-color problem, or the Kepler conjecture - both of which have been computer-verified.

[explaininjs]

> you could enumerate all possible proofs of a given length

That does not help us with proof search as we do not know the target length.

[bawolff]

A proof longer than the size of the universe is also pretty useless and probably not something we need to worry about.

Like i guess you are saying we couldn't really use such a machine to determine whether a certain conjecture just has a very long proof/disproof or is actually undecidable. Which sure, but umm i think that is the sort of problem most mathematicians would love to have.

The real reason non-deterministic turing machines can't help us is that they dont actually exist.

[dellamonica]

Of course it would, you would enumerate lengths too. If the lengths need to be larger than polynomially bounded then we can be sure it would never be found by a human anyway.