Hacker News new | ask | show | jobs
by elehack 3505 days ago
Technically, yes, but practically, no.

THEOREMS (the language of correct proofs) is in P; given a correct proof (possibly restricted to being in first-order logic), it can be verified in polynomial time. In the first-order logic case, all you have to do is read the proof from beginning to end and verify that each statement follows from either an axiom or an already-established statement. This is done entirely syntactically, requiring no knowledge of the underlying mathematics.

However, to do this requires formalizing the entire proof in machine-checkable format, which is a substantial undertaking even for relatively simple proofs and will likely take far longer than polynomial time.