Menschliche Mathematiker bei der Suche nach Gegenbeispielen von KI überholt

• Modelle der ChatGPT- und Claude-Familie haben innerhalb nur weniger Wochen Gegenbeispiele zur Einheitsdistanz-Vermutung von Erdős, zu Grothendiecks Frage zu Gruppenschemata und zur Jacobian Conjecture erzeugt; einige wurden mit Lean verifiziert
• OpenAIs Sol hat das Erdős-Gegenbeispiel und die dafür nötigen Resultate der globalen Klassenkörpertheorie in 3 Wochen in 1,2 Millionen Zeilen Lean-Code formalisiert; das ist mehr als die Hälfte der 2,3 Millionen Zeilen von mathlib, die in 9 Jahren geschrieben wurden
• Für Grothendiecks 60 Jahre alte Frage fand Sol ein 12-seitiges Gegenbeispiel, und Fable formalisierte es in 4 Stunden in 1.076 Zeilen; damit wurde die Existenz eines Gruppenschemas der Ordnung 4, das nicht von 4 vernichtet wird, bestätigt
• Automatische Formalisierung erhöht auch das Forschungstempo stark: Andrew Yang schrieb in etwa 2 Wochen 250.000 Zeilen Lean-Code und schloss damit das Projekt zum Modularitätshebungssatz, der für den Beweis von Fermats letztem Satz nötig ist, praktisch ab
• Der von KI erzeugten informellen Mathematik kann man nicht einfach blind vertrauen; wenn man Vermutungen jedoch in präzise Lean-Aussagen übersetzt, lassen sich Beweise und Widerlegungen maschinell prüfen, und Menschen müssen aus Gegenbeispielen tiefere mathematische Einsichten gewinnen

---

Erdős’ Einheitsdistanz-Vermutung und globale Klassenkörpertheorie

• Am 20. Mai 2026 widerlegte ChatGPT die Erdős-Einheitsdistanz-Vermutung aus der diskreten Geometrie
  • Das Gegenbeispiel wurde mithilfe eines tiefen zahlentheoretischen Satzes von Golod und Shafarevich aus den 1960er-Jahren konstruiert
  • Mehrere Mathematiker prüften die Argumentation vorab und hielten sie für stichhaltig, doch zum Zeitpunkt der Veröffentlichung gab es keine Lean-Formalisierung
• Am 26. Mai teilte Fields-Medaillenträger Mike Freedman, Chief Scientific Officer bei Logical Intelligence, mit, dass sein System die gesamte ChatGPT-Arbeit automatisch in Lean formalisiert habe
  • Der formalisierte Umfang war die Aussage, dass der Satz von Golod–Shafarevich das Erdős-Gegenbeispiel impliziert
  • Der zugrunde liegende zahlentheoretische Satz selbst erfordert über 100 Seiten und stützt sich auf große Teile der globalen Klassenkörpertheorie
• Im Jahr nach der Summer School zur Formalisierung der Klassenkörpertheorie 2025 war der lokale Fall fast abgeschlossen, der globale Fall blieb jedoch ungelöst

Die vollständige Formalisierung mit 1,2 Millionen Zeilen von Sol

• Am 26. Juni veröffentlichte Boris Alexeev von OpenAI im Lean-Zulip, dass er das neue Modell Sol dazu gebracht habe, eine vollständige Formalisierung des Erdős-Gegenbeispiels zu erzeugen, die außer den Axiomen der Mathematik nichts voraussetzt
• Sol erzeugte in 3 Wochen 1,2 Millionen Zeilen Lean-Code
  • mathlib, das über 9 Jahre geschrieben wurde, umfasst 2,3 Millionen Zeilen
  • Die Codequalität war uneinheitlich, doch schwierige Resultate der globalen Klassenkörpertheorie und nichttriviale Sätze über die Kohomologie von Zahlkörpern wurden tatsächlich bewiesen
• Lean ist eine Programmiersprache, die beliebige Befehle ausführen kann; wegen möglicher Schadfunktionen wurde der erzeugte Code daher in einer Sandbox ausgeführt
• Dieses Ausmaß und dieses Tempo führten zur Einschätzung, dass groß angelegte KI-generierte Mathematikentwicklung unvermeidlich ist

Workshop Formalizing Fermat und Zugänglichkeit der Werkzeuge

• Am Workshop Formalizing Fermat vom 6. bis 10. Juli nahmen 25 Personen teil, aber das automatische Formalisierungssystem des Sponsors Logos Research konnte nur von 5 Personen gleichzeitig genutzt werden
• Allen Teilnehmenden wurde ein einmonatiges Claude-Max-Abo zur Verfügung gestellt, damit sie Claude Fable nutzen konnten, und OpenAI gab ebenfalls kostenlosen einmonatigen Zugang zu ChatGPT Pro
  • Sol sollte am 9. Juli erscheinen
  • Fable sollte am 7. Juli enden, der tatsächliche Zugang blieb jedoch bestehen
  • Die Teilnehmenden konnten an 4 der 5 Workshop-Tage Sol und Fable nutzen und während des gesamten Zeitraums die Werkzeuge von Logos
• Um die Theorie endlicher flacher Gruppenschemata zu entwickeln, die für die Formalisierung von Fermats letztem Satz nötig ist, wurden klassische Arbeiten in Fable und ChatGPT eingegeben und natürlichsprachliche Erläuterungen erzeugen lassen
  • Logos fand, dass eine in den Erläuterungen enthaltene Aussage falsch war, und lieferte ein explizites Gegenbeispiel
  • Bei der Überprüfung stellte sich heraus, dass ein von einem LLM erzeugtes Dokument zur Beschreibung einer Standardkonstruktion fehlerhaft war, und Menschen hatten den Fehler beim Lesen übersehen
  • Der Unterschied bestand darin, dass nicht einfach nur geantwortet wurde, man verstehe das Argument nicht, sondern ein Beweis dafür geliefert wurde, dass das Argument falsch ist

Grothendiecks Frage zu Gruppenschemata

• Der UChicago-Professor Akhil Mathew legte der KI Grothendiecks alte Frage vor, ob jedes endliche freie Gruppenschema der Ordnung (n) durch (n) vernichtet wird
  • Deligne bewies den kommutativen Fall
  • Grothendieck bewies den Fall, in dem die Basis reduced ist
  • Rene Schoof behandelte weitere Fälle, und Emiliano Torti bewies in einer Arbeit aus dem Vorjahr noch allgemeinere Fälle
• Am 11. Juli, dem Tag nach dem Workshop, fand Sol ein Gegenbeispiel und erzeugte ein 12-seitiges PDF
  • Als statt eines informellen Resultats eine vollständige Lean-Formalisierung verlangt wurde, formalisierte Fable dies in 4 Stunden in 1.076 Zeilen automatisch
• Zunächst wurde geprüft, ob die Lean-Datei nur Sätze und keine Befehle wie Dateilöschung enthielt, bevor sie auf einem Notebook kompiliert wurde
  • Es wurde überprüft, ob für die Aussage nur Konzepte aus mathlib verwendet wurden
  • Es wurde geprüft, ob die Aussage tatsächlich die Existenz des Gegenbeispiels ausdrückte
  • Es wurde kontrolliert, ob der Beweis erfolgreich kompilierte
  • Die gesamte Verifikation dauerte weniger als 5 Minuten
• Das Ergebnis der Verifikation: Es existiert ein Gruppenschema der Ordnung 4, das nicht von 4 vernichtet wird
• Akhil Mathew reichte dieses Gegenbeispiel als mathlib-PR ein
• Während das Erdős-Gegenbeispiel rund 1 Million Zeilen umfasst, war das Grothendieck-Gegenbeispiel mit etwa 1.000 Zeilen deutlich einfacher; dennoch war es ein Fall, in dem eine Maschine eine 60 Jahre alte Frage der algebraischen Geometrie löste

Reaktionen von Fachleuten und der Modularitätshebungssatz

• Am 14. Juli bewertete ein Professor des Imperial College, dass die leichte Auffindbarkeit des Grothendieck-Gegenbeispiels nur zeige, dass Menschen über dieses Problem nicht lange genug nachgedacht hätten
• Der Doktorand Andrew Yang nutzte Sol und Fable, während er den für Fermats letzten Satz wichtigen Modularitätshebungssatz in Lean formalisierte
  • Er schrieb in etwa 2 Wochen 250.000 Zeilen Lean-Code
  • Damit schloss er das Projekt praktisch ab
• Ein anderer Professor am Imperial hielt es zunächst für schwer nachvollziehbar, dass Doktorandinnen und Doktoranden 200 Dollar im Monat für Sol und Fable zahlen, urteilte nach Prüfung dieser Ergebnisse jedoch im Gegenteil, dass es irrational sei, als Promotionsstudent nicht 200 Dollar im Monat für solche Werkzeuge auszugeben
• Harvard bot bereits allen Doktorandinnen und Doktoranden, Postdocs und Professorinnen und Professoren kostenlosen Zugang zu Fable an

Gegenbeispiel zur Jacobian Conjecture

• Akhil Mathew und Levent Alpöge diskutierten Wege, weitere Gegenbeispiele in der algebraischen Geometrie zu finden, und Fable fand ein Gegenbeispiel zur Jacobian Conjecture, einem berühmten Problem, das seit rund 100 Jahren offen war
• Levent Alpöge veröffentlichte das offenbar während des WM-Finales 2026 gelöste Resultat auf X
• Als Akhil Mathew einen neuen mathlib-PR vorschlug, hatte Paul Lezeau das Gegenbeispiel bereits manuell formalisiert und einen PR an DeepMinds Formal Conjectures Repository eingereicht
• mathlib besitzt keine große Liste mathematischer Vermutungen, aber das Formal Conjectures Repository enthält eine solche
• Wenn Menschen sich auf eine Lean-Aussage einigen, die die Bedeutung einer Vermutung getreu erfasst, wird es einfach zu prüfen, ob von KI erzeugter Code diese Vermutung beweist oder widerlegt

Was Menschen nach der formalen Verifikation noch leisten müssen

• Bei der Jacobian Conjecture besteht der nächste Schritt für Menschen darin, genau zu verstehen, was in diesem Gegenbeispiel geschieht
• Auch beim Grothendieck-Gegenbeispiel wird daran gearbeitet, über das bloße Auflisten beliebiger Ringdarstellungen und Rechnungen hinaus zu einem tieferen Verständnis zu gelangen
• Der Wert von Gegenbeispielen liegt nicht nur darin, ein Problem formal zu beenden; vollendet wird er erst im Extrahieren von Einsichten, die Menschen Mathematik besser verstehen lassen

[GN⁺]

Hacker-News-Kommentare

• Während des Graduiertenstudiums hatte ich in einem Forschungsseminar meines Betreuers die Gelegenheit, direkt zu einem offenen Problem beizutragen. An einem Freitag stellte der Professor eine glatte und schöne Vermutung vor, von der er hoffte, dass sie wahr sei, aber ich mochte seltsame Ausnahmen und hatte nicht genug Werkzeuge für Beweise, also konzentrierte ich mich darauf, ein Gegenbeispiel zu finden, und fand innerhalb einer Stunde eines
  Der Professor scheiterte das ganze Wochenende über an einem Beweis, und das zeigte, dass Menschen mit unterschiedlichen Werkzeugen, Erwartungen und Motivationen auf dasselbe Problem schauen und aus völlig verschiedenen Richtungen beitragen können. Ich kann mich nicht mit einem großen Betreuer messen, aber damals hatte ich immerhin einen Grund, in eine andere Richtung zu schauen, und das führte zu meinem einzigen kleinen mathematischen Forschungsbeitrag, einem Gegenbeispiel

  • Vermutlich ist das auch der Grund, warum Maschinen gut darin sind, Gegenbeispiele zu finden. Sie haben keine ästhetische Fixierung auf eine Vermutung und schämen sich nicht, hässliche Resultate auszugeben
  • Als Mathematiker ist mein Eindruck eher das Gegenteil. Einen Beweis kann man oft durch leichte Abwandlung eines bekannten Beweises erhalten, aber um ein Gegenbeispiel zu konstruieren, muss man die Struktur des Objekts tief verstehen, und das übersteigt oft meine Fähigkeiten
    Das kann allerdings daran liegen, dass ich mich meist mit abstrakten Objekten beschäftige, die schwer zu verstehen sind; bei Zahlen oder Polynomen könnte es umgekehrt sein
  • Professoren, Forschende und Lehrkräfte, die Studierenden noch ungelöste Probleme offen zeigen und sie zur Mitarbeit ermutigen, sollten viel mehr Wertschätzung bekommen. Als in meiner ersten Ingenieurvorlesung an der Universität der Dozent den Erstsemestern sagte: „Das sind Probleme, die wir noch nicht gelöst haben, also sagt Bescheid, wenn euch eine Idee kommt“, fühlte ich mich so willkommen und als Teil der Gemeinschaft wie nie zuvor, und es war in der leicht langweilig werdenden frühen Studienphase eine große Inspiration
  • In How to Solve It gibt es fast genau dieselbe Geschichte
  • Es gibt eine extremere und entgegengesetzte Anekdote über Zeeman. Er verbrachte Jahre damit, in einem 5-dimensionalen Raum eine verknotete Sphäre zu finden, erkannte dann, dass das unmöglich war, und bewies es in wenigen Stunden
    https://ima.org.uk/28009/sir-erik-christopher-zeeman-the-mat...

• Yitang Zhang, bekannt für die Vermutung über Primzahlzwillinge, arbeitete an Purdue unter der Betreuung von Tzuong-Tsieng Moh sieben Jahre lang an der Jacobi-Vermutung. Es stellte sich heraus, dass ein Schlüsselschritt seiner Dissertation auf einem falschen Korollar von Moh beruhte, Moh weigerte sich, ein Empfehlungsschreiben zu verfassen, und Zhang konnte keine Lehr- oder Forschungsstelle finden und arbeitete jahrelang bei Subway
  Ich frage mich, wie es gewesen wäre, wenn es 1986, als er seine Forschung begann, schon ChatGPT gegeben hätte. Heute ist es eine bewegende Erfolgsgeschichte, aber wie der Vers „庾信平生最萧瑟，暮年诗赋动江关“ weckt sie komplexe Gefühle

  • Ich habe erlebt, dass ein Prüfer während einer Mathematik-Promotion einen Fehler im Beweis entdeckte. Nachdem der Student es verstanden hatte, fragte er: „Und was machen wir jetzt?“, worauf der Prüfer nur mit den Schultern zuckte
  • Man kann sagen, dass es bewegend ist, weil er später bei der Vermutung über Primzahlzwillinge Erfolg hatte, aber ich bin solche Geschichten aus der Wissenschaft leid. Es gibt zu viel Politik und Reputationsmanagement, und Zhang hätte dieses Leid nicht durchmachen sollen
    Als ich meine Forschung stärker auf Mathematik ausweitete, war ich überrascht, wie viele Aussagen in der Literatur falsch sind und wie weit sie sich sogar in die angewandte Literatur verbreitet haben. Selbst wenn man auf Probleme hinweist, reagieren viele wie in Zhangs Geschichte mit Abwehr und Leugnung. LLMs sind für Beweise nützlich, liegen aber auch massiv daneben und ähneln eher einer weiteren Person, die aus einer anderen Intuition heraus Suchrichtungen vorschlägt, daher wäre das Ergebnis 1986 vermutlich dasselbe gewesen
  • Die Bedeutung des von ChatGPT übersetzten Verses ist ungefähr: „Yu Xins Leben war durch und durch trostlos, doch seine Gedichte und Fu-Dichtungen im Alter erschütterten Flüsse und Grenzlande.“

• In der Mathematik sind Gegenbeispiele sehr wichtig, um Definitionen zu verfeinern und Beweise zu schärfen. Ich empfehle Imre Lakatos’ Buch Proofs and Refutations von 1976, und in Gebieten wie Topologie, Wahrscheinlichkeitstheorie und Analysis gibt es auch ziemlich viele Bücher, die sich nur mit Gegenbeispielen befassen
  https://en.wikipedia.org/wiki/Proofs_and_Refutations
  https://www.amazon.com/s?k=counterexamples

• Wenn man ein Gegenbeispiel findet, verschwendet man keine Zeit damit, eine falsche Aussage zu beweisen, und kann zu einem anderen Problem übergehen; zumindest in der Mathematik hilft das also, die Zeit der Menschheit produktiver zu nutzen

  • Widerlegung durch Gegenbeispiel ist effektiv, aber letztlich nicht zufriedenstellend. Sie gibt eine Antwort, lässt einen aber nicht verstehen, warum die Mathematik so funktioniert, und führt auch nicht zu neuen Fragen
    Solange Menschen beurteilen, was ein eleganter und aufschlussreicher Beweis ist, wird es Arbeit für menschliche Mathematiker geben
  • Gegenbeispiele sind auch nützlich, um die Aussage eines Satzes zu präzisieren. In der theoretischen Informatik ist es üblich, einen Satz beweisen zu wollen, ein Gegenbeispiel zu finden, die Aussage zu ändern und dann weiterzumachen
    Hilfreich ist auch, dass viele Sätze in der Informatik induktive und koinduktive Definitionen behandeln
  • Besonders wenn ein Gegenbeispiel formal verifiziert ist, kann es jahrelange spekulative Bemühungen fast sofort in eine definitive Antwort verwandeln
  • Insgesamt kann man aber nicht einfach behaupten, dass die Zeit dadurch produktiver genutzt wurde. Ob man eine Aussage beweist oder widerlegt, ob sie am Ende wahr oder falsch ist: Im Prozess können neue Einsichten entstehen

• Offenbar wird auch die mathematische Version der Ballad of John Henry von KI geschrieben werden. Ich frage mich, wer der letzte menschliche Champion sein wird, der einen Beweis liefert, „der in THE BOOK stehen könnte“, und den selbst Maschinen nicht übertreffen
  https://en.wikipedia.org/wiki/John_Henry_(folklore)
  https://en.wikipedia.org/wiki/Proofs_from_THE_BOOK

  • Das ist eine ungesunde Sichtweise, die Mathematik wie Fußballfanatiker als Wettbewerb betrachtet. Das Wertvollste in der Mathematik sind nicht nur schöne Beweise, sondern nützliche Definitionen, und gute Definitionen sowie daraus gute Vermutungen zu machen ist ein Bereich, den LLMs noch nicht zu erobern versuchen
  • Noch ist es nicht ganz so dramatisch, aber bald könnte dieser Punkt erreicht sein. Es gibt keine strukturelle Grundlage, um vorherzusagen, ob sich die Fähigkeiten von KI asymptotisch verbessern oder beschleunigen werden, und beide Möglichkeiten bleiben offen, welche Probleme durch neue Methoden lösbar werden
    Wir verstehen weder das Innere der KI-Fähigkeiten noch ihre Wachstumskurve, und wir wissen nicht einmal genau, ob sie ihre Leistung absichtlich schlechter erscheinen lässt. Es könnte ein emergentes Phänomen sein, das sich Messungen entzieht, oder in ein paar Jahren so vorhersagbar wie ein Uhrwerk werden. Niemand weiß es, und wenn doch, sagt er es nicht, und auch die Lautesten wissen nichts

• Wenn damit sinnvolle Leistungen von Doktorand:innen deutlich früher erreicht werden, gibt es keinen Grund, nicht 2.400 $ pro Student und Jahr zu investieren. Im Verhältnis zu den Gesamtkosten ist das fast Kleingeld.

  • Einige Doktorand:innen sehen sich nicht als „Maschinen zur Produktion sinnvoller Ergebnisse“, sondern als moralische Wesen. Alle wissen, dass selbst nützliche LLMs wegen gestohlener Trainingsdaten und der enormen Umweltbelastung schwer zu rechtfertigen sind.
  • Das EPSRC-Lebenshaltungsstipendium für Promotionsstudierende liegt bei etwa 20.000 £ und entspricht damit ungefähr 10 % der jährlichen Kosten. Für die einzelnen Studierenden ist das eine große Belastung.

• Während des Studiums hätte ich mir von LLMs erzeugte Lean-Formalisierungen gewünscht. In der Mathematik auf den Vorlesungsfolien gab es viele Fehler, und einige Professoren lehnten Erklärungen mit dem Hinweis ab, „der Beweis steht auf den Folien“, während sie Fehler nur widerwillig eingestanden.
  Lean-Beweise selbst eignen sich oft nicht besonders gut zum Verständnis, aber ich hoffe, dass man darauf aufbauend menschenfreundlichere Argumentationen erzeugen kann.

  • Der ersten Behauptung stimme ich nur schwer zu. Die Lernkurve ist steil, aber gut geschriebene Lean-, Agda- und Rocq-Formalisierungen sind hervorragend geeignet, um Beweise zu verstehen. Gute Formalisierungen zeigen Überblick und Kernargumente strukturell und erlauben es im Gegensatz zu Papierbeweisen, die Details jedes Schritts bis in jede gewünschte Tiefe zu prüfen.
    Das Agda-Repository TypeTopology von Martín Escardó ist ein gutes Beispiel. Dagegen können von heutigen LLMs erzeugte Formalisierungen sehr chaotisch sein; selbst wenn sie Sätze verifizieren und interessante Argumente enthalten, ist oft erhebliche Arbeit nötig, um sie in eine Form zu bringen, die das mathematische Verständnis verbessert. Ein interaktives Agda-Tutorial gibt es unter lets-play-agda.quasicoherent.io.
  • Formalisierungen lassen sich auch für einen Leibnizschen Ansatz nutzen, der Debatten beendet und Zweifel vollständig beseitigt.

• Ich frage mich, ob Gegenbeispiele für Mathematiker so sind wie unerwartete Resultate in den Naturwissenschaften — zunächst lästig, aber enorm wichtig, weil sie Ungenauigkeiten eines Modells offenlegen — oder eher wie Bug-Reports in der Programmierung, also nebensächliche und lästige Details.

  • Gegenbeispiele machen die Rolle von Bedingungen klar. Es ist sehr nützlich, die einfachsten und einprägsamsten Gegenbeispiele zu haben, die zeigen, was scheitert, wenn man jede einzelne Bedingung eines Beweises verletzt.
    Mathematiker tragen oft einen Zoo von Gegenbeispielen im Kopf mit sich herum. Wenn sie einen Satz rekonstruieren, erinnern sie sich an prägnante, einprägsame Gegenbeispiele und können Definitionsbereich und Bedingungen so einschränken, dass diese ausgeschlossen werden.
  • Es gibt Lehrbücher wie Counterexamples in Topology und Counterexamples in Analysis, die die Feinheiten eines Fachgebiets anhand von Gegenbeispielen vermitteln. Sie sind beliebt, weil man Details oft leichter an pathologischen oder degenerierten Beispielen lernt als nur an den beabsichtigten Standardobjekten.

• Ein großer Teil dieser Mathematik ist schwer zu verstehen, scheint sich aber meist mit dem Beweisen von Sätzen zu beschäftigen. Falls sich KI-Mathematik weiter beschleunigt, frage ich mich, ob sie irgendwann sogar neue Mathematik entdecken wird, die in Technik oder Biomedizin Anwendung findet — ob wir kurz vor einem großen Durchbruch der Menschheit stehen oder ob es dabei bleibt, bereits Bekanntes zu beweisen.

  • Die Möglichkeit besteht. Compressed Sensing kann als Beispiel für neue Mathematik gelten, die in der Biomedizin Anwendung findet; es kann die Dauer von MRT-Aufnahmen stark verkürzen, die Erfahrung für Patient:innen verbessern und mehr Untersuchungen ermöglichen.
    https://en.wikipedia.org/wiki/Compressed_sensing
  • Selbst wenn es Anwendungen in Technik und Biomedizin geben wird, dürfte das eher langfristig sein; die Entwicklung neuer mathematischer Methoden könnte jedoch früher für die Grundlagenforschung in der Physik wichtig werden. Häufig haben neue mathematische Werkzeuge, die die Darstellung oder Überprüfung von Kosmosmodellen ermöglichten, zu deutlichen Verbesserungen dieser Modelle geführt.
  • Selbst wenn es möglich ist, wird es sehr lange dauern. In den meisten Anwendungsfeldern fangen wir gerade erst an, sogar Mathematik von vor mehreren Jahrhunderten richtig zu nutzen.

• Irgendwann könnten Mathematiker unter der Last zu prüfender Beweise begraben werden, und durch Übervertrauen könnten falsche Behauptungen in die Mathematik einsickern. Künftige Mathematiker prüfen dann vielleicht wie Softwareingenieure, die KI verwenden, tausende Zeilen KI-generierter Beweise und suchen nach subtilen Fehlern.

  • Dieser Zeitpunkt ist längst gekommen. Die heutige Literatur ist riesig und voller fehlerhafter Beweise, und unter den veröffentlichten Resultaten gibt es — in unbekannter, aber sicher nicht null großer Zahl — auch falsche Resultate.