Hilbert II

Ziel des Projekts Hilbert II ist der freie und dezentrale Zugang zu verifiziertem und lesbarem mathematischem Wissen. Dieses Projekt steht, wie der Name schon andeutet, in der Tradition von Hilberts Programm.

Hilbert II will eine weltweite mathematische Wissensbasis sein, die mathematische Sätze und Beweise in formal korrekter Form enthält. Alle zugehörigen Dokumente werden unter der GNU Free Documentation License veröffentlicht. Wir wollen die übliche mathematische Argumentation in eine formale Syntax überführen. D. h., wann immer in der Mathematik eine bestimmte Argumentation häufig benutzt wird, wird sie in die formale Sprache von Hilbert II integriert. Diese formale Sprache wird hier auch als QEDEQ-Format bezeichnet.

Hilbert II stellt eine Programmsuite zur Verfügung, die es einer Mathematikerin ermöglicht Propositionen und Beweise dieser Wissensbasis hinzuzufügen. Dabei werden die Beweise automatisch auf Korrektheit überprüft. Auch Texte in "normaler mathematischer Sprache" können eingebunden werden. Die mathematischen Axiome, Definitionen und Sätze sind in sogenannten QEDEQ-Modulen zusammengefasst. Ein solches Modul kann auch als mathematisches Textbuch aufgefasst werden, das formal korrekte Beweise enthält. Da das System nicht zentral adminstriert wird und Verweismöglichkeit auf andere QEDEQ-Module überall im Internet möglich sind, kann ein weltweites mathematisches Wissensnetz aufgebaut werden. Jeder Beweis einer Proposition in diesem Wissensnetz kann auf die ganz elementaren Regeln und Axiome und Definitionen zurückgeführt werden. Im Idealfall gibt es eine riesige Anzahl von mathematischen Textbüchern mit Querverweisen und jeder vorkommende Beweis kann durch Hilbert II auf Korrektheit überprüft werden. Auch die Abhängigkeit von anderen Propositionen, Definitionen und Axiomen kann auf einfache Weise ermittelt werden.

Das Hauptprojekt befindet sich noch in der Entwicklung, aber die aktuelle Anwendung kann schon via Java-Web-Start gestartet werden. Weitere Informationen sind unter Status and Planung zu finden.

Es gibt auch einen funktionierenden Prototypen der den Namen Principia Mathematica II trägt. Er beherrscht die Prädikatenlogik erster Stufe und besitzt die Haupteigenschaften von Hilbert II. Er kann (prototypspezifische) QEDEQ-Moduldateien, die sich irgendwo im Internet befinden, auf formale Korrektheit überprüfen. Der Prototyp besitzt eine GUI und kann QEDEQ-Module in HTML- und LaTeX-Dateien umwandeln. Es kann auch ein eigenes QEDEQ-Modul erzeugt, editiert und dann ins Internet gestellt werden. Bereits im Netz befindliche QEDEQ-Module können durch einfache Referenzierung benutzt werden.