Computer-Aided Verification of Existing P/NP Proof Attempts

The notorious P/NP question is among the most challenging open problems of computer science, and one of the remaining six unsolved millennium problems of the Clay Institute. Despite the progress made in decades ever since the problem was posed, the question has so far not been answered. It is easy to describe intuitively: consider only problems whose answer is simply yes or no. Among these, consider those for which a yes/no answer is computable in reasonable time, depending on the size of the problem. Call the class of all these problems P. Now, suppose that we do not ask for how to find a solution, because we are already given one. Then, the challenge is to verify if the solution at hand is correct or not, and many problems admit such a check efficiently. Put these problems into the class NP. The P/NP question is whether P = NP, or if these two classes are distinct, or as a third possibility if neither the equality nor inequality can be proven at all. The apparent simplicity of the problem has attracted many researchers to look into the issue, ranging from professional scientists, up to hobby mathematicians, having come up with a vast variety of proposed solutions to the question, none of which has yet been approved by the scientific community. A few barriers and dead-ends towards an answer are known, but the simple lot of proposed proofs of either P = NP or P NP is growing faster than people can verify them. This creates an unpleasant situation that may, in the long run, practically lead to the correct answer perhaps coming up, but go unrecognized among the many wrong attempts. As of today, there are more roughly 120 proof attempts available, with a mild majority claiming that P NP, a slight minority claiming P = NP, and very few ones saying that this is eventually not provable. Given that todays scientific quality management heavily depends on peer review, often done by people on voluntarily basis (and hence without revenue), the project seeks to empower people to getting an independent and objective verification of their work with help from computers. Specifically, we will pick a few published proof attempts from all three categories (equal, not equal, unprovable), model them in a machine-readable representation and let computers verify the mathematical arguments. Such proof assistants are useful to mathematicians to let complex logical reasoning be handed over to machines for an objective judgement without the need to find voluntary peer reviewers. Irrespectively of its meaning for science, P/NP is an invaluable question to study, and has been a source and inspiration of many new concepts and ideas that have found applications elsewhere. Making P/NP proofs machine-verifiable (much in the spirit of how the class NP itself is defined) may not only be a step towards an answer to the question itself, but also contributes to proof assistants themselves as being powerful tools in research.

Computer science offers efficient algorithms for solving a wide range of problems. This includes calculation problems, optimisation problems but also pure decision problems whose answer is simply "yes" or "no". The class "P" specifically includes the latter decision problems, provided they can be solved in a "reasonable" amount of time, i.e. with a realistic amount of resources in terms of time and memory. The class NP has problems to which solutions are known but not always reachable with contemporary resources. Nevertheless, many of the decision problems contained in NP allow a very efficient verification of a given solution. Examples of this include the travelling salesman problem (finding the shortest route through a series of cities without visiting a city twice), or placing people around a round table so that the individual wishes regarding left and right neighbourhood are taken into account (known as the Hamilton circle problem). Despite their apparent simplicity, these and many other problems escape all attempts at an efficient solution. The P/NP problem is the question of whether problems for which a given solution can be checked quickly also allow such a solution to be found just as efficiently. This question, which has been unanswered for decades, was declared one of the 6 Millennium Problems and is considered one of the most fundamental problems in computer science. Especially because of its intuitive simplicity, a large number of authors, both inside and outside the scientific community, have tried to find a solution, and as of autumn 2023, more than 120 proof attempts have been published. None of these have yet convinced the scientific community, and the large number of failed attempts has meant that valuable resources have sometimes been sparsely invested in reviewing newly submitted papers. Although the verification of new theoretical results is essential, this part of scientific activity enjoys a comparatively lower prestige and reputation than finding new results. The conduct of both by the same person(s) would be desirable, but is not necessarily equally objective. The CAVE PNP project therefore aims to investigate the feasibility of checking mathematical proofs in the context of P/NP using computer-aided proof assistants. These are specialised programming languages that can reproduce, semi-automatically find or check the concepts, structures and chains of reasoning of mathematical proofs. This enables authors to check their own work independently, since a computer-aided verification does not tolerate formal inaccuracies. The majority of scientists "believes" that P and NP are distinct; a slightly smaller lot believes in the equality, and a few papers claim the general unanswerability of the question. Time will eventually settle the problem, but the ability for an objective self-review by proof assistants may pave the way and speed up the search.