Die Mathematik ist vom Nimbus der Unfehlbarkeit umgeben: schon in der Schule lernen wir, dass mathematische Entdeckungen ewige Gültigkeit haben. Ein Blick in die Geschichte der Mathematik zeigt aber, dass es durchaus allgemein anerkannte mathematische Resultate gab, die sich als falsch erwiesen, sowie mathematische Theorien, in denen Widersprüche entdeckt wurden.
Der Grund dafür, dass trotz der theoretischen Unfehlbarkeit des Beweises Irrtümer auftreten, ist, dass Mathematiker genau genommen nur Beweisskizzen formulieren, die wir im Folgenden informelle Beweise nennen. Damit die Beweise nicht zu umfangreich werden, ist es gängig, Sprünge in der Beweisführung zu machen, die durch abstrakte Argumente gerechtfertigt werden, deren Überprüfung selbst für einen Experten viel Arbeit erfordert. Ob ein Beweis tatsächlich korrekt ist, und damit, ob ein mathematischer Satz als bewiesen gilt, entscheidet die Forschungsgemeinschaft heutzutage durch Peer-Review-Verfahren. Hierbei besteht natürlich Raum für Fehlentscheidungen.
Informelle Beweise lassen sich jedoch prinzipiell in formale Beweise umformen. Ein formaler Beweise beginnt mit Axiomen und leitet aus diesen die zu beweisende Konklusion ab, wobei jeder Schritt der Beweisführung die Anwendung einer genau definierten logischen Deduktionsregel ist. Solche Beweise können von Computern auf Korrektheit überprüft werden und außerdem können Computer selbst formale Beweise generieren. Damit ist der Ansatz, in der mathematischen Praxis informelle durch formale Beweise zu ersetzen, in zweierlei Hinsicht reizvoll: zum einen würden die von Mathematikern erbrachten Ergebnisse wegen der Ablösung des Peer-Reviews durch computergestützte Überprüfung den Status der Unfehlbarkeit, der ihnen prinzipiell zukommt, erhalten. Zum anderen ergibt sich die Möglichkeit, dass Computer in Zukunft interessante Resultate automatisch beweisen, oder zumindest das Beweisen von Hilfsresultaten übernehmen. Mit dem Gödelschen Vollständigkeitssatz wurde die Umsetzbarkeit dieses Ansatzes auch theoretisch erwiesen. Beispiele, wie der computergestützte Beweis der Andrew-Robbins-Vermutung im Jahr 2011, an der sich namhafte Mathematiker jahrzehntelang vergeblich versucht hatten, sind Belege für den praktischen Nutzen von computergestützter Mathematik.
Der Preis dafür, dass man mathematische Beweise auf die unanzweifelbare Ebene der logischen Deduktion zurückführt, ist, dass bereits für einfache Resultate die Beweise so lang werden, dass sie für Menschen schwer nachvollziehbar sind. Dies erklärt warum, auch nachdem eine Gruppe von Mathematikern, darunter insbesondere David Hilbert, in den 1930er Jahren die Möglichkeit der formalen Mathematik sehr plausibel machten, sich diese nicht durchsetzen konnte: die Idee schien praktisch nicht realisierbar. Was damals utopisch galt, scheint heutzutage angesichts der Verfügbarkeit von leistungsfähigen Computern zwar näher gerückt zu sein. Allerdings schaffen es heutige automatische Beweiser selbst mit großer Rechenkapazität nicht, für viele der für menschliche Mathematiker trivialen Aussagen, formale Beweise zu finden. Genau dies ist aber eine Voraussetzung für die Umsetzung der formalen Mathematik: menschliche Mathematiker können unmöglich den gesamten formalen Beweis aufschreiben, sondern lediglich einzelne Meilensteine desselben ausarbeiten; die Schritte dazwischen müssen vom Computer bewiesen werden. An dieser Stelle gibt es also algorithmische Probleme, die die Informatik lösen muss. Neben diesen praktischen Grenzen gibt es auch theoretische Grenzen dafür, was für Aussagen man in einer Theorie formal beweisen kann, wie der Gödelsche Unvollständigkeitssatz zeigt. Außerdem ergibt sich aus wissenschaftsphilosophischer Sicht die Frage, ob die formale Mathematik tatsächlich auf einem stabileren erkenntnistheoretischen Fundament steht, als die derzeitige Mathematik. Statt auf menschlichen Verstand verlässt sie sich darauf, dass die Computerprogramme fehlerfrei sind, die die Beweise überprüfen und generieren. Und selbst wenn alle Hindernisse überwunden werden könnten, und eine Revolution in der mathematischen Praxis möglich wäre, stellt sich aus wissenschaftssoziologischer Sicht die Frage, ob die mathematische Community einen solchen Paradigmenwechsel akzeptieren würde. Heutzutage jedenfalls lässt sich beobachten, dass die Perspektive einer formalen Mathematik für viele Mathematiker entweder als utopisch gilt, oder aber als bedrohlicher Versuch gesehen wird, die Menschen in der Mathematik durch Computer zu ersetzen.
Trotz dieser theoretischen und praktischen Einschränkungen lassen die Erfolge der formalen Mathematik der letzten Jahre darauf schließen, dass sie ein Thema von wachsender Bedeutung ist. Im Rahmen des Seminars möchten wir der Notwendigkeit einer interdisziplinären Behandlung des Phänomens Rechnung tragen, indem wir Wissenschaftler und Studenten aus Mathematik, Informatik, Philosophie und Soziologie zusammenbringen, um die Grenzen und Möglichkeiten der formalen Mathematik zu diskutieren.
Der Grund dafür, dass trotz der theoretischen Unfehlbarkeit des Beweises Irrtümer auftreten, ist, dass Mathematiker genau genommen nur Beweisskizzen formulieren, die wir im Folgenden informelle Beweise nennen. Damit die Beweise nicht zu umfangreich werden, ist es gängig, Sprünge in der Beweisführung zu machen, die durch abstrakte Argumente gerechtfertigt werden, deren Überprüfung selbst für einen Experten viel Arbeit erfordert. Ob ein Beweis tatsächlich korrekt ist, und damit, ob ein mathematischer Satz als bewiesen gilt, entscheidet die Forschungsgemeinschaft heutzutage durch Peer-Review-Verfahren. Hierbei besteht natürlich Raum für Fehlentscheidungen.
Informelle Beweise lassen sich jedoch prinzipiell in formale Beweise umformen. Ein formaler Beweise beginnt mit Axiomen und leitet aus diesen die zu beweisende Konklusion ab, wobei jeder Schritt der Beweisführung die Anwendung einer genau definierten logischen Deduktionsregel ist. Solche Beweise können von Computern auf Korrektheit überprüft werden und außerdem können Computer selbst formale Beweise generieren. Damit ist der Ansatz, in der mathematischen Praxis informelle durch formale Beweise zu ersetzen, in zweierlei Hinsicht reizvoll: zum einen würden die von Mathematikern erbrachten Ergebnisse wegen der Ablösung des Peer-Reviews durch computergestützte Überprüfung den Status der Unfehlbarkeit, der ihnen prinzipiell zukommt, erhalten. Zum anderen ergibt sich die Möglichkeit, dass Computer in Zukunft interessante Resultate automatisch beweisen, oder zumindest das Beweisen von Hilfsresultaten übernehmen. Mit dem Gödelschen Vollständigkeitssatz wurde die Umsetzbarkeit dieses Ansatzes auch theoretisch erwiesen. Beispiele, wie der computergestützte Beweis der Andrew-Robbins-Vermutung im Jahr 2011, an der sich namhafte Mathematiker jahrzehntelang vergeblich versucht hatten, sind Belege für den praktischen Nutzen von computergestützter Mathematik.
Der Preis dafür, dass man mathematische Beweise auf die unanzweifelbare Ebene der logischen Deduktion zurückführt, ist, dass bereits für einfache Resultate die Beweise so lang werden, dass sie für Menschen schwer nachvollziehbar sind. Dies erklärt warum, auch nachdem eine Gruppe von Mathematikern, darunter insbesondere David Hilbert, in den 1930er Jahren die Möglichkeit der formalen Mathematik sehr plausibel machten, sich diese nicht durchsetzen konnte: die Idee schien praktisch nicht realisierbar. Was damals utopisch galt, scheint heutzutage angesichts der Verfügbarkeit von leistungsfähigen Computern zwar näher gerückt zu sein. Allerdings schaffen es heutige automatische Beweiser selbst mit großer Rechenkapazität nicht, für viele der für menschliche Mathematiker trivialen Aussagen, formale Beweise zu finden. Genau dies ist aber eine Voraussetzung für die Umsetzung der formalen Mathematik: menschliche Mathematiker können unmöglich den gesamten formalen Beweis aufschreiben, sondern lediglich einzelne Meilensteine desselben ausarbeiten; die Schritte dazwischen müssen vom Computer bewiesen werden. An dieser Stelle gibt es also algorithmische Probleme, die die Informatik lösen muss. Neben diesen praktischen Grenzen gibt es auch theoretische Grenzen dafür, was für Aussagen man in einer Theorie formal beweisen kann, wie der Gödelsche Unvollständigkeitssatz zeigt. Außerdem ergibt sich aus wissenschaftsphilosophischer Sicht die Frage, ob die formale Mathematik tatsächlich auf einem stabileren erkenntnistheoretischen Fundament steht, als die derzeitige Mathematik. Statt auf menschlichen Verstand verlässt sie sich darauf, dass die Computerprogramme fehlerfrei sind, die die Beweise überprüfen und generieren. Und selbst wenn alle Hindernisse überwunden werden könnten, und eine Revolution in der mathematischen Praxis möglich wäre, stellt sich aus wissenschaftssoziologischer Sicht die Frage, ob die mathematische Community einen solchen Paradigmenwechsel akzeptieren würde. Heutzutage jedenfalls lässt sich beobachten, dass die Perspektive einer formalen Mathematik für viele Mathematiker entweder als utopisch gilt, oder aber als bedrohlicher Versuch gesehen wird, die Menschen in der Mathematik durch Computer zu ersetzen.
Trotz dieser theoretischen und praktischen Einschränkungen lassen die Erfolge der formalen Mathematik der letzten Jahre darauf schließen, dass sie ein Thema von wachsender Bedeutung ist. Im Rahmen des Seminars möchten wir der Notwendigkeit einer interdisziplinären Behandlung des Phänomens Rechnung tragen, indem wir Wissenschaftler und Studenten aus Mathematik, Informatik, Philosophie und Soziologie zusammenbringen, um die Grenzen und Möglichkeiten der formalen Mathematik zu diskutieren.
