Computer-Aided Verification of Existing...

Ziel des Projekts ist eine Auswahl vorhandener Arbeiten bzgl. des P/NP-Problems auszuwählen, und die darin enthaltenen Argumente von einem (maschinellen) Beweis-Assistenten überprüfen zu lassen. Es geht hierin nicht darum, eine Antwort auf die offene Frage selbst zu finden, sondern die „Masse“ an vorgeschlagenen Beweisen nicht nur manuell, sondern mit maschineller Unterstützung einer Begutachtung unterziehen zu können. Wenn die Anzahl an Beweisvorschlägen schneller wächst, als wissenschaftliches Peer-Review die Arbeiten begutachten und ggf. Fehler identifizieren können, dann besteht die Möglichkeit, dass die Antwort tatsächlich gefunden wird, jedoch in der Masse (fehlerhafter) Ansätze unerkannt untergeht. Diesem Umstand soll mit Unterstützung von Computern, insbesondere Beweisassistenten, entgegengewirkt werden.            

Auswahlkriterien für untersuchte Publikationen (Beweisansätze) sind unter anderem (i) die Strenge der Argumentation, (ii) die Eignung der angewendeten Beweis-Techniken, (iii) die Durchführbarkeit der Modellierung und (iv) das behauptete Ergebnis der Relation von P zu NP (gleich/ungleich/unbeweisbar).            

Erwartete Ergebnisse: Forscher*innen, die sich mit der Frage beschäftigen sollen erweiterte Möglichkeiten erhalten, ihre Ideen und Argumente einer maschinellen, und damit einer objektiv/unabhängigen, Prüfung zu unterziehen (vor einer Veröffentlichung). Unabhängig hiervon dient die P/NP Frage somit als „Studienobjekt", dessen Untersuchung die Möglichkeiten maschineller Beweisverifikation voranbringen soll, letztlich zur Unterstützung, Vereinfachung und Objektivierung wissenschaftlicher Peer-Reviews.