> In short, being able to automatically decide the validity of a proof is almost as useful as being able to generate a valid proof automatically.
This statement is not known to be true, and is definitely false in practice at the moment. Validating proofs is a P complexity task, so generating proofs is by definition NP, very likely NP-complete.
How does this have to do with "practice at the moment"? Don't you mean "practice" as in what people actually do, in practice? I don't understand where complexity comes in to that. From what I can tell, work in generating new proofs, in the style of Logic Theorist, has dried up and interactive theorem provers are very popular, even among some mathematicians, so they clearly are useful.
Anycase, far be it from me to discourage opportunistic nitpicking or pedantry, my favourite sports, but, amicably, I don't understand what you are trying to tell me. I'm curious and I'd like to know. If you have the time and patience, please clarify.
Trivial? I don't think so. I mean, the article above describes a new state of the art established by a large language model trained with much expense and effort that achieved a measly 50% ish score.
But in any case, I think you are trying to say that if something has polynomial time complexity then it's not useful, compared to a problem for which we don't know a polynomial time algorithm. I don't think that works out like that. For example, we have sorting algorithms with polynomial time complexity and I don't think anyone would say they're not useful.
They generate proofs in the article, not validate existing ones. The algorithm to validate a proof is known and AFAIK does not need much improvement (e.g. it is already practical).
You're right, the trained models evaluated in the paper did not perform proof
verification, which was handled by an external, hand-crafted Metamath
verifier.
However, the trained models didn't generate new _proofs_ either. Rather, they
assigned log-probabilities to proof _steps_ (a substitution unifying a theorem
to a goal) and the log-probabilities were then used to select the best next
goal to expand during a traditional, hand-crafted best-first search (the
authors say that the search ended up being breadth-first "most of the time",
but it was coded as best-first, from their descriptions).
Anyway this is a bit sideways to your point. I still think you're nitpicking
about my use of the word "useful" and applying it without much sensibility to
an argument about complexity that you are interested in. I didn't say anything
about complexity. I said that proof verficiation is very useful. I also don't
agree that it's "trivial". There are simple enough algorithms to perform it,
but, for example, Metamath's "variable substitution" is, from what I can say,
essentially unification and while unification is efficient, it was only
described - I was going to say by Robinson, but Wikipedia tells me that
Herbrand had a unification algorithm before that, which was still quite late
in the history of mathematics (early 20th century). Your comment above about
how proof verification is "trivial" is only true in hindsight.
I said above I don't mind nitpicking, but I'm actually getting a bit tired
with it. My original comment made a point about the lack of clear motivation
in the discussed paper. Your comment chose to address tiny point made as an
aside and in response to another comment. What is the purpose of that? What
have we learned from this discussion about the triviality of proof
verification and the NP-completeness of proof generation? Was this a
productive exchange for either of us, or was the whole point of this to show
off how much we respectively know to make the other commenter feel a fool?
This statement is not known to be true, and is definitely false in practice at the moment. Validating proofs is a P complexity task, so generating proofs is by definition NP, very likely NP-complete.