|
|
|
|
|
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. |
|