Am 20. Juli 2026 schrieb Kevin Buzzard, Mathematikprofessor am Imperial College London, einen Blogbeitrag, der seine Kollegen schmerzhaft direkt traf: Menschliche Mathematiker werden von Gegenbeispielen überholt. Der Grund: Die KI hatte innerhalb von nur zwei Monaten drei mathematische Vermutungen widerlegt, die jahrzehntelang ungelöst waren – eine davon fast ein Jahrhundert alt.
Buzzard selbst sagt: »Ich habe weniger als fünf Minuten gebraucht, um ein seit 60 Jahren offenes algebraisch-geometrisches Gegenbeispiel zu verifizieren. Ich lud den Lean-Code auf meinen Laptop herunter, die Kompilierung lief durch, und ich nickte: Ja, das ist tatsächlich ein Gegenbeispiel.«
Fünf Minuten. Das ist die Trennlinie zwischen menschlicher und KI-gestützter Mathematik. Dieser Artikel beleuchtet, wann diese Grenze gezogen wurde und was sie bedeutet.
Gegenbeispiele: Ein schärferes Messer als Beweise
Zunächst ein Grundkonzept. In der Mathematik ist es schwer, eine Aussage zu beweisen – man muss eine lückenlose Herleitung liefern, bei der jeder Schritt stimmt. Eine Aussage zu widerlegen ist jedoch vergleichsweise einfach: Man braucht nur ein Gegenbeispiel – eine konkrete Konstruktion, die alle Voraussetzungen erfüllt, aber nicht die Schlussfolgerung.
Wenn jemand sagt: »Alle Schwäne sind weiß«, muss man nicht jeden Schwan der Welt überprüfen. Ein einziger schwarzer Schwan genügt.
Ein Gegenbeispiel kann jahrelange Forschung zunichtemachen. Und genau deshalb spielen Gegenbeispiele in der Mathematikgeschichte eine kreative Rolle – sie zeigen, wo die Grenzen einer Theorie liegen, zwingen Mathematiker, Annahmen zu überdenken, Definitionen zu verbessern und Theorien weiterzuentwickeln. In gewisser Weise sind Gegenbeispiele der Treibstoff des mathematischen Fortschritts.
Die KI treibt diese Kunst, »schwarze Schwäne« zu finden, auf eine ungeahnte Ebene.
Mai bis Juli 2026: Der Dreifachschlag der KI
Im Folgenden eine chronologische Übersicht der Ereignisse der letzten drei Monate.
Erster Schlag: Die Erdős-Unit-Distance-Vermutung (1946 aufgestellt, am 20. Mai 2026 widerlegt)
Die diskret-geometrische Frage, die der legendäre Mathematiker Paul Erdős 1946 formulierte. ChatGPT lieferte eine Gegenbeispiel-Konstruktion. Buzzards erste Reaktion: »Wurde das in Lean verifiziert?« Nein. Doch weniger als eine Woche später schickte Fields-Medaillen-Gewinner Mike Freedman (inzwischen Chief Scientific Officer bei der KI-Firma Logical Intelligence) eine E-Mail – ihr System hatte die Argumentation automatisch in Lean-Code übersetzt.
Einen Monat später vollendete Boris Alexeev von OpenAI mit dem neuen Modell Sol die Arbeit: Das gesamte Gegenbeispiel wurde ausgehend von den mathematischen Axiomen vollständig formalisiert. Sol erzeugte dafür 1,2 Millionen Zeilen Lean-Code.
Zum Vergleich: Die Mathematik-Bibliothek mathlib, die von der Lean-Community in neun Jahren aufgebaut wurde, umfasst insgesamt nur 2,3 Millionen Codezeilen. Die KI generierte in drei Wochen mehr als die Hälfte dessen, was Menschen in neun Jahren geschaffen haben. Buzzards Kommentar fiel knapp aus: »Massiv KI-generierte Mathematik ist unvermeidlich geworden.«
Zweiter Schlag: Das Grothendieck-Gruppenschema-Problem (1960er Jahre, am 11. Juli 2026 widerlegt)
Grothendieck ist einer der bedeutendsten Mathematiker des 20. Jahrhunderts. Vor 60 Jahren stellte er die Frage: Wird ein endliches freies Gruppenschema der Ordnung n notwendigerweise durch n annihiliert? Deligne bewies den Fall kommutativer Gruppenschemata, Grothendieck selbst den Fall reduzierter Basisringe – aber die vollständige Aussage blieb offen.
Sol fand ein Gegenbeispiel. Der gesamte Beweis umfasst nur 1076 Zeilen Lean-Code. Buzzard brauchte weniger als fünf Minuten, um alles zu verifizieren. Er schlug dem Mathematiker Akhil Mathew vor, das Gegenbeispiel in die Mathematik-Bibliothek aufzunehmen – und scherzte: »Versuchst du als Nächstes die Hodge-Vermutung?«
Dritter Schlag: Die Jacobi-Vermutung (1939 aufgestellt, am 19. Juli 2026 widerlegt)
Dies war der schwerste Schlag. Die Jacobi-Vermutung (Jacobian Conjecture) ist eine Umkehrfrage polynomieller Abbildungen: Wenn die Jacobi-Determinante einer polynomiellen Abbildung eine von Null verschiedene Konstante ist, ist die Abbildung dann notwendigerweise umkehrbar? Diese Frage hielt sich seit 1939 und gilt als eine der verführerischsten und hartnäckigsten Vermutungen der algebraischen Geometrie.
Dieses Mal war es Claude Fable von Anthropic, das zuschlug. Es fand das Gegenbeispiel während des Finales der Fußball-Weltmeisterschaft 2026. Am nächsten Tag veröffentlichte Terence Tao – einer der angesehensten Mathematiker der Gegenwart – einen detaillierten Blogbeitrag, der das Gegenbeispiel mathematisch »verdaut«.
Taos Berechnungen zeigen: Das Gegenbeispiel ist eine polynomiale Abbildung mit drei Variablen und maximal siebter Ordnung. Ihre Jacobi-Determinante ist −2 – erfüllt also die Bedingung einer von Null verschiedenen Konstanten – aber die Abbildung bildet drei verschiedene Eingabepunkte auf denselben Ausgabepunkt ab, ist also nicht injektiv und damit nicht umkehrbar. Noch erstaunlicher: Die KI nutzte 120 einstellbare Parameter, um die theoretisch möglichen 1329 Koeffizienten der Jacobi-Determinante so zu kontrollieren, dass alle Nicht-Null-Terme einander exakt aufhoben. In Taos Worten: »Das wirkt wie ein gewaltiges Wunder.«
Lean + LLM: Die Verbindung von Kreativität und mathematischer Strenge
Nach der Geschichte nun zur technischen Logik.
Lean ist ein »Mathematik-Compiler«. Schreibt man einen mathematischen Beweis in Lean, muss jede einzelne Ableitung einen strikten Typprüfungstest bestehen. Es gibt keine »offensichtlichen Schritte« – alles Offensichtliche muss auf atomarer Ebene ausgeführt werden. Wenn der Code kompiliert, ist der Beweis mathematisch absolut korrekt – ohne dass ein menschlicher Gutachter vertrauen muss.
Das LLM (Large Language Model) übernimmt das Konzipieren, Lean das Urteilen. Die inhärente Schwäche von LLMs in der Mathematik ist ihre Neigung zum Erfinden – sie produzieren auch dann plausible Argumentationsketten, wenn sie keine Ahnung haben. Lean behebt dieses Problem grundlegend: Das LLM generiert Lean-Code, der Compiler prüft sofort. Wenn die Kompilierung fehlschlägt, erhält das LLM die Fehlermeldung und kann korrigieren. Iterativ, bis der Code kompiliert – an diesem Punkt hat das KI-generierte mathematische Ergebnis eine strenge Korrektheitsgarantie.
Im März 2026 erschien ein Paper mit dem Titel »Learning to Disprove«, das diese Methodik systematisch darlegte. Die Kernidee: Statt ein LLM zu beauftragen, einen Satz zu beweisen (was zum Erfinden verleitet), soll es Gegenbeispiele suchen – denn sobald ein Gegenbeispiel in Lean kompiliert, ist es unwiderlegbar. Die Autoren verwendeten eine Strategie der »Symbolvariation«, bei der systematisch bestimmte Bedingungen aus bestehenden Theoremen entfernt werden, um Trainingsdaten für die Gegenbeispielsuche zu erzeugen. Ein Multi-Reward-Mechanismus trainierte das LLM. Ergebnis: Die Trefferquote bei der Generierung von Gegenbeispielen stieg um 49 %.
Das ist die technische Grundlage des »Gegenbeispiel-Überholens«: Das LLM liefert die Kreativität, Lean die mathematische Strenge, und der menschliche Mathematiker wird zum Zuschauer – zumindest bei der Ergebnisfindung.
Die fünf Phasen der Trauer in der Mathematik-Community
Buzzard hält in seinem Blogbeitrag offen die Reaktionen seiner Kollegen fest. In der Mittagspause am Imperial College hörte er einen Kollegen sagen: »Wenn Gegenbeispiele so leicht zu finden sind, bedeutet das nur, dass die Menschen nicht genug Zeit darauf verwendet haben.« Er lächelte innerlich – er selbst hatte einst eine ganze Woche in genau dieses »nicht lohnende« Problem investiert.
Das ist die typische Phase der Verleugnung.
Danach kam das Feilschen. Ein Professor schickte erstaunt eine E-Mail: Warum zahlen Doktoranden freiwillig 200 Dollar im Monat für Sol und Fable? Buzzards Antwort war direkt: »Jeder Doktorand, der diese 200 Dollar nicht investiert, handelt irrational.« Die Harvard-Universität hat inzwischen allen Mathematik-Doktoranden, Postdoktoranden und Lehrkräften kostenlosen Zugang zu Fable gewährt.
Unabhängig von den Emotionen ist eine Tatsache klar: In der mathematischen Forschung klafft die Kluft zwischen denen, die KI-Tools beherrschen, und denen, die es nicht tun, monatlich weiter auseinander.
Die Richtung, die Tao vorgibt
Unter allen Reaktionen ist die von Terence Tao vielleicht die bemerkenswerteste. Er stellt weder die Fähigkeiten der KI in Frage, noch verliert er sich in philosophischen Debatten darüber, ob das noch Mathematik sei. Er setzte sich hin und schrieb einen detaillierten Blogbeitrag, berechnete die gewichtete Homogenität des Polynoms, lieferte eine geometrische Neuinterpretation und veröffentlichte sogar das vollständige Transkript seiner Diskussion mit GPT-5.
Dies ist die typische Haltung eines Mathematikers an der Front: Die Ergebnisse liegen auf dem Tisch – erst verstehen, dann nutzen.
Tao schrieb in der HN-Diskussion: »Es zeigt uns, dass scheinbar unmögliche mathematische Konstruktionen in einem ausreichend großen Suchraum gefunden werden können.« Die versteckte Botschaft dieses Satzes: Der Suchraum ist zwar riesig, aber die KI hat uns gelehrt, wie wir suchen müssen. Und das ist erst der Anfang.
Was bleibt den Mathematikern?
Wenn KI Gegenbeispiele finden, Beweise verifizieren und ganze Theorien automatisch formalisieren kann – was bleibt dann noch für den Menschen?
Buzzards Antwort: Verstehen und Erklären. Er sagt: »Der wahre Wert dieser außergewöhnlichen Beispiele liegt darin, dass sie uns ein tieferes Verständnis der Mathematik vermitteln können.« Akhil Mathew versucht bereits, die Struktur hinter dem Grothendieck-Gegenbeispiel aus einer tieferen Perspektive zu verstehen – er fragt nicht nur »Ist das eine zufällige Konstruktion?«, sondern »Was passiert hier eigentlich wirklich?«
Die KI kann dir sagen, dass etwas nicht stimmt. Aber sie kann dir oft nicht sagen, was das für unser mathematisches Weltbild bedeutet.
Historisch gesehen haben Mathematiker das Rechnen immer wieder an Maschinen ausgelagert und sich dann auf die höheren Ebenen des Verstehens und Konstruierens konzentriert. Jetzt können auch das Finden von Gegenbeispielen und das Verifizieren von Beweisen ausgelagert werden. Was bleibt, ist genau das, was vielleicht der Kern der Mathematik ist: Wenn die Maschine das Gegenbeispiel auf den Tisch legt, wirklich zu verstehen, warum es bedeutsam ist – und was wir daraus lernen können.
Das ist nicht das Ende der Mathematik. Aber die Rolle des Mathematikers durchläuft eine irreversible Evolution.
Referenzen:
- Xenaproject – Kevin Buzzards ursprünglicher Blogbeitrag »Human Mathematicians Are Being Outcounterexampled«
- HN-Diskussion (id: 48998362) – Community-Diskussion zu Terence Taos Blogbeitrag über die Jacobi-Vermutung
- Lobsters-Diskussion (s/wfmpqr) – Technische Community-Kommentare zu KI-generierten Gegenbeispielen
- Terry Taos Blogbeitrag – Verdauung und mathematische Rekonstruktion des Jacobi-Gegenbeispiels
- SBSeminar – Mathematische Detail-Diskussion des neuen Jacobi-Gegenbeispiels
- arXiv 2603.19514 – Learning to Disprove: Formale Gegenbeispiel-Generierung mit LLMs
- New Scientist – KI löst 87 Jahre altes Mathematikproblem
- GitHub DeepMind Formal Conjectures – Formales Vermutungs-Repository mit Jacobi-Gegenbeispiel
