Dreizehn Jahre Stillstand – jetzt könnte ein Schiedsrichter kommen. Wie New Scientist berichtet, nutzen zwei unabhängige Projekte jetzt Lean, einen Beweisassistenten, um Shinichi Mochizukis 500-seitige ABC-Vermutungs-Beweis maschinell zu verifizieren – eines dieser Projekte läuft bereits über zwei Jahre im Verborgenen. Falls Lean einen Urteilspruch fällt, wird das die folgenreichste Anwendung formaler Verifikation in der modernen Mathematik sein. Und für alle in AEC, die algorithmische Ausgaben für strukturelle, regulatorische oder Compliance-Entscheidungen nutzen, reichen die Implikationen weit über Zahlentheorie hinaus.

←TODAY: Zwei Lean-Formalisierungsprojekte sind live; Mochizuki selbst endorset Lean als einzige Technologie, um den Streit ohne soziale oder politische Einmischung zu klären.
→3012: Zurich-3012-Baugenehmigungen: maschinell ausgestellt gegen formal verifizierte Strukturbeweise; keine menschliche Freigabeschleife.
Fulcrum: Der Moment, da ein Computer einen Fields-Medaillen-Träger in mathematischer Autorität überragt, ist der Moment, da algorithmisches Vertrauen zu institutioneller Infrastruktur wird.

Die Vorgeschichte: präzise zu kennen. 2012 postete Mochizuki seinen Beweis online – aufgebaut auf einem völlig eigenständigen theoretischen Rahmen, den er Inter-universelle Teichmüller-Theorie (IUT) nannte. Der Rahmen brauchte Jahre an Vorbedingungen, nur um sich zu nähern. Breites mathematisches Verständnis kam nie. 2018 kündigten Peter Scholze (Universität Bonn) und Jakob Stix (Goethe-Universität Frankfurt) an – beide Grössen der europäischen Mathematik, Scholze Fields-Medaillen-Träger 2018 – dass sie einen spezifischen Fehler identifiziert hatten. Mochizukis Kyoto-Kreis behauptete, der Beweis sei korrekt. Die breitere Gemeinschaft schloss: bestenfalls unverständlich. Das Patt verhärtete.

Was das Patt aufbrach – oder zumindest eine Tür öffnete – ist die Reife der Beweisformalisierung. Tools wie Lean, Coq und Isabelle übersetzen schriftliche mathematische Argumente in maschinell überprüfbaren Code, der entweder kompiliert oder nicht. Es gibt keinen Raum für »Ich denke, dieser Schritt ist plausibel.« Lean insbesondere wurde bereits eingesetzt, um bedeutende zeitgenössische Ergebnisse zu verifizieren: Scholze selbst nutzte es für das Liquid Tensor Experiment, eine hochkarätige Formalisierung seiner eigenen Arbeit in kondensierter Mathematik. Diese Geschichte macht seine implizite Befürwortung der Methode, selbst als Skeptiker der IUT, ein strukturell wichtiges Signal. Mochizukis eigene Aussage – dass Lean »die beste und vielleicht einzige Technologie… zur Erreichung bedeutsamen Fortschritts zum Ziel der Befreiung mathematischer Wahrheit vom Joch sozialer und politischer Dynamik« ist – ist eine ungewöhnlich direkte Aussage für einen Mathematiker über Software.

Die Geheimhaltung um eines der beiden Projekte ist aufschlussreich. Wer es leitet, arbeitete zwei Jahre lang ohne öffentliche Überprüfung – das deutet auf institutionelle Vorsicht vor voreiligen Ergebnissen hin, oder Empfindlichkeit gegenüber dem politischen Temperament des Streits, oder beides. Keine Namen, keine Zwischenergebnisse, kein Zeitplan sind publik. Diese Opazität selbst ist ein Datenpunkt: die Einsätze sind hoch genug, dass die Projektleiter beschlossen, das Risiko eines Lecks wiegt schwerer als der Nutzen offener Wissenschaft.

Atelier: Die BIM-Parallele ist exakt, nicht metaphorisch. Wenn ein parametrisches Modell für Peer Review zu komplex wird – wenn kein einzelner Ingenieur in einem Projekt die vollständige Logik eines 15.000-Element-Grasshopper-Scripts im Kopf halten kann – ist die Verifikationsfrage dieselbe, der Mochizukis Rezensenten gegenüberstehen. Leans Ansatz (maschinell überprüfbar, regelbasiert, eindeutig) ist strukturell gleich wie Clash Detection oder Code-Compliance-Prüfung in einem BIM-Workflow. Falls formale Verifikation einen Streit von 13 Jahren zwischen Fields-Medaillen-Trägern klären kann, wird die Argumentation, diese Methode zur Strukturzertifizierung und behördlicher Genehmigung in der Schweiz und der EU einzuführen, erheblich schwerer zu widerlegen.

Das Risiko deutlich: Eine Lean-Verifikation ist nur so zuverlässig wie die Formalisierung selbst. 500 Seiten IUT in Maschinencode zu übersetzen erfordert menschliche Entscheidungen bei jedem Schritt – welche Definitionen, wie informale Intuition in formale Syntax übersetzt. Eine Formalisierung kann intern konsistent sein und trotzdem den mathematischen Punkt verfehlen. Der Computer versteht die Vermutung nicht; er überprüft den Code. Diese Lücke ist real. Wer versucht ist, eine erfolgreiche Lean-Kompilation als finales Urteil zu nehmen, sollte die Lean-Dokumentation lesen, nicht bloss die Pressemitteilung.

Für Schweizer und DACH-Profis: ETH Zürich und EPFL forschen beide aktiv an formalen Methoden und Beweisassistenten, aber es gibt keinen bestätigten direkten Einfluss in den IUT-Projekten. Das europäische Gewicht – Scholze Bonn, Stix Frankfurt – bedeutet: jede Auflösung landet in Forschungskultur, die mit Schweizer akademischen Netzwerken überlappt. Beobachten Sie die Preprint-Server. Wenn eines dieser Projekte publik wird, ist das kein stilles Statement.

Anfang hier: Der Lean-Beweisassistent ist Open Source und dokumentiert auf leanprover.github.io. Falls Ihr Büro komplexe parametrische oder Struktur-Scripts laufen lässt, die kein Team-Mitglied vollständig auditen kann, nehmen Sie sich dreissig Minuten Zeit, um zu verstehen, was formale Verifikation tut. Die ABC-Vermutung mag abstrakt sein; das Verifikationsprinzip nicht.

Quelle: New Scientist