Computer-Aided Verification of Existing P/NP Proof Attempts
Project Description
Computer-Aided Verification of Existing P/NP Proof Attempts
The goal of the project is to select a sample of existing papers concerning the P/NP problem and to have the arguments contained therein checked by a (machine) proof assistant. The aim is not to find an answer to the open question itself, but to be capable to examine the "mass" of proposed proofs not only manually, but with machine support. If the number of suggested proofs grows faster than scientific peer review can assess the work and identify possible errors, then there is a possibility that the solution is actually found, but is lost in the mass of (incorrect) approaches. This situation should be counteracted with the support of computers, in particular proof assistants.
The publications examined (proof approaches) are selected with respect to the following aspects (i) the rigor of the argumentation, (ii) the proof techniques applied, (iii) "feasibility" of modeling in proof assistants, and (iv) the claimed result of the relation of P to NP (equivalent/indifferent/unprovable).
Expected results: Researchers who deal with the question should be given extended possibilities to subject their ideas and arguments to a mechanical, and thus objective/independent, examination (before publication). Independently of it the P/NP question serves thus as "study object", whose investigation is to advance the possibilities of mechanical proof verification, as an aid, simplification and objectification of scientific Peer reviews.
Duration
24 months
Keywords
complexity theory, proof assistant, P/NP