Computer-Aided Verification of Existing P/NP Proof Attempts
Projektbeschreibung
Computer-Aided Verification of Existing P/NP Proof Attempts
Ziel des Projekts ist eine Auswahl vorhandener Arbeiten bzgl. des P/NP-Problems zu identifizieren, 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.
Aktuelles: Siehe unsere [github Organisation](https://github.com/CAVE-PNP) für Ergebnisse der Formalisierung. Entsprechende Publikationen sind aktuell (Stand November 2023) in Begutachtung.
Fördergeber
CAVE-PNP ist gefördert durch den Fonds zur Förderung der wissenschaftlichen Forschung (FWF) im 1000 Ideen Programm
Dauer
24 Monate
Schlagworte
complexity theory, proof assistant, P/NP