\begin{center} Wahrheit und Verifikation
\end{center}
\begin{center}
  Pr"ufen  mathematischer Argumentationsketten mit  Rechenmaschinen.
\end{center}
Bei der Wahl einer griffigen "Uberschrift f"ur diesen Einblick in
neuere Entwicklungen im Zugang zur Mathematik habe ich meiner Lust zur
Alliteration freien Lauf gelassen. Wahrheit ist aber selbst in der
Mathematik ein schillernder Begriff.
In der Formalisierung der Mathematik, wie sie zu Beginn des vergangenen
Jahrhunderts entwickelt wurde, spricht man lieber von \glqq Beweis\grqq\ und
\glqq Beweisbarkeit\grqq\ im Rahmen eines vorgegebenen \glqq Axiomensystems\grqq\ 
und setzt die Theorie so auf, da"s die Korrektheit eines Beweises
im Prinzip von 
einer Rechenmaschine "uberpr"uft werden kann. Daf"ur werden mathematische
Behauptungen kodiert als Zeichenketten  aus endlich vielen durch das
Axiomensystem  erlaubten Zeichen wie zum Beispiel die Kette
$$((a|p) \RA (a=p\lor a=1))\RA ((p|bc)\RA (p|b\lor p|c))$$
Sie ist zusammengesetzt aus den Zeichen $ a,b,c,p,\RA,(,),\lor,1,=$.
Als entsprechend vorgebildeter Mensch wei"s man, da"s das
 Symbol $\lor$ in diesem Kontext vermutlich 
 \glqq oder\grqq\ bedeutet. Man 
 mag mit diesem und weiterem Hintergrundwissen
 unsere Zeichenkette interpretieren als die Behauptung, da"s
 wenn eine Primzahl 
 ein Produkt teilt, da"s sie dann auch einen der Faktoren teilt.
 Unsere Rechenmaschine aber interpretiert nicht, sie rechnet.
 \\[2mm]\noindent
Ein Axiomensystem gibt uns au"ser den erlaubten Zeichen auch eine
 Liste von Zeichenketten, die unsere Rechenmaschine a priori als bewiesen ansehen darf, die \glqq Axiome\grqq.  Ein Axiomensystem gibt uns
 schlie"slich sogenannte
 \glqq Schlu"sregeln\grqq, die Situationen spezifizieren,
 in denen das Pr"adikat \glqq bewiesen\grqq\ von zwei Zeichenketten
 auf eine Dritte "ubertragen werden darf. Sind zum Beispiel $A,B$ bewiesene
 Zeichenketten und geh"ort auch $\land$ zu den erlaubten Symbolen,
 so kann unser Axiomensystem vorsehen, da"s
 dies Pr"adikat von den Zeichenketten $A$ und $B$ auf die Zeichenkette
 $(A)\land(B)$
 "ubertragen werden darf. Als Mensch mag man sich dabei denken, da"s wenn
 $A$ und $B$ wahre Behauptungen sind, da"s dann auch ($A$ und $B$) eine
 wahre Behauptung sein mu"s. Unsere Rechenmaschine aber
 denkt nicht, sie rechnet.
 \\[2mm]\noindent
 Wenn wir eine Rechenmaschine entsprechend programmieren, so kann sie
 unsere Beweise "uberpr"ufen, indem sie "uberpr"uft,  ob wir
 dabei von den Axiomen ausgehend die Schlu"sregeln korrekt angewandt haben.  
 Sogar jede beweisbaren Zeichenketten
 wird sie  irgendwann finden, aber bei den meisten Axiomensystemen
 ist nicht vorherzusehen, wie lange das dauern wird und wieviel Speicher
 sie daf"ur ben"otigt.
 Und bereits 1931 ver"offentlichte Kurt G"odel seinen ber"uhmten Unvollst"andigkeitssatz, nach dem es in jedem Axiomensystem,
 das die Arithmetik der nat"urlichen Zahlen beschreiben kann,   
 entweder einen Widerspruch oder eine unentscheidbare Behauptung geben
 mu"s. Wir wissen also schon seid bald hundert Jahren, da"s es
 mit der Wahrheit auch in der Mathematik nicht so einfach ist.
 \\[2mm]\noindent
Die neuere Entwicklung, "uber die ich hier berichten will, besteht darin,
 da"s man nichttriviale Beweise nicht nur im Prinzip,
 sondern auch in der Praxis
 mit Rechenmaschinen "uberpr"ufen kann und "uberpr"uft.
Die Motivation daf"ur liegt in der "uberbordenden
Komplexit"at der modernen Mathematik. Im Prinzip ist nat"urlich, Hand aufs Herz,  
jede ver"offentlichte Arbeit von einem Referenten auf
ihre Korrektheit gepr"uft worden oder zumindest darauf gepr"uft worden,
da"s sie korrekt ist unter der Annahme, da"s alle darin aus anderen
bereits ver"offentlichten Arbeiten herbeizitierten Resultate
ihrerseits korrekt sind. In der Praxis aber sind bei diesem Vorgehen  
Fehler unvermeidbar und umso wahrscheinlicher, je l"anger die
Argumentationsketten werden.
 \\[2mm]\noindent
Die Klassifikation der einfachen endlichen Gruppen etwa, ein gro"sartiges
Resultat der Algebra, hat einen Beweis von gut 10000 Seiten,
verteilt "uber Forschungsartikel in gut 100 Zeitschriften.
Bereits 1981 hie"s es, der Beweis sei nun vollst"andig.
Bei einer gro"s angelegten Revision traten dann aber ernste Probleme zu Tage,
die erst 2004 in einer weiteren Arbeit von "uber 1000 Seiten behoben werden konnten. Die Revision des Beweises ist immer
noch nicht abgeschlossen, der Initiator dieses
Projekts ist nicht mehr am Leben und die beiden anderen treibenden
Kr"afte gehen beide auf die Achzig zu, und es gibt weitere "ahnlich gelagerte F"alle. 
In so einer Situation w"are es nat"urlich schon
w"unschenswert,   die Argumentation
mit Hilfe einer Rechenmaschine zu verifizieren.
Zumindest f"ur einen ersten Teil des Beweises  ist das 2012
mit dem Beweisassistenten Coq unter der Federführung von
Georges Gonthier durchgef"uhrt
worden\footnote{Gonthier, G. et al. (2013). A Machine-Checked Proof of the Odd Order Theorem.}.
 \\[2mm]\noindent
Ein anderer bekannter Fall ist der Beweis von Thomas Hales
einer Vermutung von Johannes Kepler, nach der es keine dichtere Kugelpackung
im dreidimensionalen Raum gibt als eben die offensichtliche Kugelpackung,
nach der im Supermarkt die Orangen gestapelt werden. Die Arbeit wurde
1998 eingereicht und ein Team von zw"olf renommierten Gutachtern besch"aftigte sich
mehrere Jahre intensiv mit dem Manuskript, um schlie"slich zu dem Schlu"s
zu kommen, sie seien zu 99\% sicher, da"s der Beweis richtig sei.
Die Arbeit wurde schlie"slich
2004 in der renommiertesten Zeitschrift ver"offentlicht,
die die Mathematik zu bieten hat, und der Autor machte sich daran, seinen
Beweis zu formalisieren. Das gelang 2014 mit der Hilfe von vielen Koautoren
und zwei anderen rechnergest"utzten 
Be\-weis\-assis\-ten\-ten mit den Namen Isabelle und HOL Light\footnote{Hales, T.  et al: A formal proof of the Kepler conjecture. Forum of Math., Pi (2017), Vol. 5}.

Ein weiteres Programm zur Verifikation von Beweisen namens
Lean hat j"ungst f"ur Furore gesorgt, weil es  meinem Freiburger
Kollegen Johan Commelin und seinen Koautoren gelungen ist, damit 2022 in k"urzester Zeit eine
frisch entwickelte Theorie von Peter Scholze zu "uberpr"ufen\footnote{https://leanprover-community.github.io/blog/posts/lte-final/}. Scholze,
der 2018 mit der Fields-Medaille ausgezeichnet wurde,
hatte selbst um eine "Uberpr"ufung gebeten,
weil ihm sein eigener Beweis zu komplex wurde.
 \\[2mm]\noindent
Aber wie k"onnen wir uns nun sicher sein, da"s diese
Verifikationen tun, was sie sollen? Das Prinzip  ist,
da"s man nur ein sehr kleines Programm ben"otigt, um zu pr"ufen,
da"s in einem formalen Beweis die Schlu"sregeln korrekt angewandt
wurden. Nur diesem kleinen Programm mu"s man vertrauen und kann damit
nach und nach und in Zusammenarbeit mit Gleichgesinnten
rund um den Globus immer umfassendere Bibliotheken
von verifiziert beweisbaren Behauptungen erstellen.  
 \\[2mm]\noindent
Ich erwarte, da"s der Verifikation von Beweisen durch Rechenmaschinen
eine wachsende Rolle
bei der weiteren Entwicklung der Mathematik zukommen wird.
Der Traum eines  Mathematikers bleibt weiterhin,
sich und andere durch Einfachkeit und Transparenz zu "uberzeugen.
Aber bei der Suche nach den sch"onen Wahrheiten werden wir
die Hilfe der Rechenmaschinen brauchen, um uns nicht in der Komplexit"at
der Argumentationsketten zu verlieren. Ich bin zuversichtlich,
da"s ein besseres Verst"andnis und tiefere Einsicht folgen werden, sobald wir erst einmal wissen, was wahr -- pardon, beweisbar ist.  
 \\[5mm]\noindent
Hier noch einige Ideen f"ur Bilder oder Graphiken. 
\begin{enumerate}
\item Foto von Kurt G"odel, von der entsprechenden
deutschen Wikipedia-Seite herunterkopiert.
\item
  Eine Kugelpackung, das Bild von
  Wikipedia \glqq Sphere Packing\grqq.
\item  Der Abh"angigkeitsgraph des Beweises des \glqq Liquid Tensor Experiment\grqq\ 
\url{https://leanprover-community.github.io/liquid/dep_graph_section_1.html}
\end{enumerate}