LLM-Vermutungen vs. Beweisprüfung: Wer gewinnt?

Irgendwo zwischen dem zweiten und dritten Kaffee hat in letzter Zeit wohl so mancher Komplexitätstheoretiker einen Satz gelesen, mit dem er nie gerechnet hätte: Ein deterministischer Algorithmus zählt die erfüllenden Belegungen einer beliebigen booleschen Formel in einer Zeit von ungefähr 2^(n/√(log n)) — subexponentiell, und zwar in dem präzisen technischen Sinn, der die Exponential Time Hypothesis widerlegt, eine der tragenden Annahmen des Fachs. Die Behauptung stammt nicht von einer Universitätsgruppe auf dem arXiv. Sie kommt von einem KI-Labor, der Beweis wurde gemeinsam mit einem großen Sprachmodell entwickelt. Was man sonst auch von der Ankündigung halten mag: Sie markiert den Moment, in dem Vermutungsgenerierung — Maschinen, die neue Mathematik vorschlagen, statt sie nur zu bewerten — das Demo-Stadium verlassen hat.

Das Labor hat drei Ergebnisse gebündelt: den komplexitätstheoretischen Knaller von oben, einen behaupteten Beweis der Kakeya-Vermutung in allen Dimensionen und ein Physikresultat, das als einheitliche Vervollständigung des Standardmodells beschrieben wird und bis zur formalen Verifikation zurückgehalten wird. Die Reaktion folgte einem vertrauten Muster: echtes Staunen über die Substanz, echter Ärger über die Verpackung. Kritiker verglichen es mit einem Fahrradhersteller, der seine eigenen Siege bei Radrennen verkündet. Treffend — und doch verdient die Substanz einen genaueren Blick, denn in dieser Ankündigung steckt eine echte Lehre über die zwei sehr unterschiedlichen Arten, wie Sprachmodelle heute die Mathematik berühren, und darüber, welcher davon man tatsächlich trauen sollte.

Was die KI-Mathematik-Ankündigung tatsächlich behauptet

Beginnen wir mit dem Komplexitätsergebnis, denn dort stehen die klarsten Einsätze auf dem Spiel. Die Exponential Time Hypothesis besagt grob, dass 3-SAT nicht in 2^o(n) Zeit lösbar ist — kein Algorithmus kann in der Anzahl der Variablen nennenswert subexponentiell sein. Hunderte Arbeiten in der parametrisierten und feingranularen Komplexitätstheorie stützen sich auf ETH, um untere Schranken zu beweisen; es ist genau die Art Annahme, auf die man ein ganzes Forscherleben voller „unter der Annahme von ETH“-Sätze stapelt. Das neue Preprint beschreibt einen deterministischen Zählalgorithmus für k-CNF-Formeln, der polynomiellen Speicher benötigt und in der Zeit 2^(n/(log n)^(1/2+o(1))) läuft, multipliziert mit einem polynomiellen Faktor. Dieser Exponent ist o(n), und genau das verbietet ETH. Der Algorithmus ist nach wie vor brutal langsam — auf einer realen Instanz wird ihn niemand je laufen lassen —, aber asymptotisch ist er entscheidend. Falls der Beweis hält, hört eine Hypothese, die zwei Jahrzehnte lang Untere-Schranken-Argumente strukturiert hat, einfach auf zu existieren.

Die zweite Behauptung zielt auf die Kakeya-Vermutung, ein Problem der geometrischen Maßtheorie über die kleinsten Mengen, die ein Einheitsliniensegment in jeder Richtung enthalten. Der dreidimensionale Fall fiel erst 2025, in einem gefeierten Beweis von Hong Wang und Joshua Zahl, den viele als Krönung einer Karriere betrachteten. Die Ankündigung behauptet einen Beweis in allen Dimensionen, was den Durchbruch vollständig einschließen würde. Das dritte Ergebnis aus der Quantenfeldtheorie ist das vagste der drei: beschrieben als „einheitliche Vervollständigung des Standardmodells“, aber noch nicht veröffentlicht und offenbar auf eine maschinell überprüfte Formalisierung wartend. Physiker, die die Teaser lesen, vermuten eher etwas aus der Familie der großen vereinheitlichten Konstruktionen als eine wörtliche Theorie von allem, und die Formulierung verdient einiges an berechtigtem Stirnrunzeln.

Zwei Dinge am Rollout verdienen Anerkennung. Das Labor hat arbeitende Mathematiker und Physiker vor der Veröffentlichung eingebunden — eine direkte Reaktion auf den Gegenwind nach einer früheren, plumperen Mathe-Ankündigung, woraufhin Terence Tao und andere öffentlich genau diese Art der Zusammenarbeit einforderten. Und das Physikergebnis wurde zurückgehalten, bis die Formalisierung abgeschlossen war, was die richtige Reihenfolge der Prioritäten ist. Doch harte Fragen bleiben offen: Niemand außerhalb kennt die Rechnung für die Rechenleistung, ob dieselben Mittel, in menschliche Forschende investiert, dieselben Sätze hervorgebracht hätten, oder ob ein gewinnorientiertes Labor die neugetriebene Grundlagenarbeit weiter finanziert, sobald die Aktionäre mitreden. Dazu kommt die unbequeme Schleife, auf die Kritiker sofort hingewiesen haben: Diese Modelle wurden teils mit den Fragen, Entwürfen und Forenbeiträgen genau jener Forschungsgemeinschaft trainiert, die nun den Output bejubeln soll.

Beweisprüfung vs. Vermutungsgenerierung: zwei verschiedene Aufgaben

Entfernt man den Hype, erledigt jedes KI-System für Mathematik eine von zwei Aufgaben. Aufgabe eins ist Beweisprüfung: Gegeben ein Argumentvorschlag, entscheide, ob er gültig ist. Aufgabe zwei ist Vermutungsgenerierung: Gegeben ein Problemgebiet, schlage vor, was sich zu versuchen lohnt — ein Lemma, eine Konstruktion, einen Algorithmus, ein Gegenbeispiel. Das klingt nach zwei Hälften einer einzigen Fähigkeit. Sind sie aber nicht. Es sind unterschiedliche algorithmische Probleme mit verschiedenen Orakeln, verschiedenen Fehlermodi und grundverschiedenen Vertrauensprofilen, und wer sie vermischt, vertraut entweder einer Pressemitteilung zu sehr oder tut echte Fortschritte ab.

Beim Prüfen gibt es ein Orakel. Ein in Lean geschriebener Beweis kompiliert gegen den Kernel oder eben nicht, und der Kernel kümmert sich nicht darum, wie sicher der Autor geklungen hat. Prüfung scheitert laut — ein abgelehnter Taktikblock ist eindeutig. Bei der Generierung gibt es kein Orakel. Eine vorgeschlagene Vermutung kann wahr, falsch, trivial wahr oder wahr und 1987 unter anderer Notation veröffentlicht sein. Generierung scheitert leise, und ihre Fehlermodi sind sozialer Natur: plausibel klingender Unsinn oder echte Ergebnisse, die als Neuheit verkauft werden. Qualität misst sich hier an Bedeutung und Originalität — Eigenschaften, die durch menschlichen Geschmack definiert sind und nicht durch ein entscheidbares Kriterium.

Warum wurde die Generierung plötzlich gut genug, um zu zählen? Weil moderne Reasoning-Modelle für lange Gedankenketten trainiert werden, nicht nur durch Prompting dorthin gelenkt — Reinforcement Learning mit überprüfbaren Belohnungen, meist in Mathematik und Code, wo sich Antworten maschinell prüfen lassen, hat diesen Systemen beigebracht, tatsächlich einen Raum von Schritten zu durchsuchen, statt nur einen nach dem anderen zu vervollständigen. Hier ist die Analogie, die ich im Kopf behalten würde: Der Beweisprüfer ist ein Compiler, der Vermutungsgenerator ist ein Designer. Beide sind wertvoll. Man würde dem Designer niemals, wirklich niemals erlauben, seine eigene Arbeit abzunehmen.

Ein Beweis, den man nicht prüfen kann, ist eine Predigt; eine Vermutung, die man nicht testen kann, ist ein Gerücht.

Wo die automatische Beweisprüfung gewinnt

Der Prüfer gewinnt überall dort, wo es eine formale Grundwahrheit gibt und das zu prüfende Artefakt für einen Menschen zu lang oder zu mühsam ist, um es Zeile für Zeile zu auditieren. Lean 4 und seine Community-Bibliothek Mathlib sind hier zur De-facto-Arena geworden: Man schreibt Definitionen und Beweise in einer Programmiersprache, und ein kleiner, separat prüfbarer Kernel entscheidet, ob jeder Schritt zulässig ist. Die vertrauenswürdige Basis ist winzig im Vergleich zum Berg an Mathematik, der darauf aufgebaut ist, und genau diese Asymmetrie will man haben.

Die praktische Schleife sieht so aus: Das Modell entwirft taktische Beweisschritte, der Kernel akzeptiert oder verwirft jeden einzelnen, und die Ablehnungsmeldungen werden als Kontext für den nächsten Versuch zurückgespeist. Dies ist der eine Fall, in dem sich die Beschränkung der Modellausgabe auf eine strikte Grammatik sofort auszahlt — man zieht nur syntaktisch gültige Taktiken, sodass ganze Klassen von Halluzinationen per Konstruktion unmöglich werden. Ein minimales Beispiel, die Art Lemma, die ein Modell heute in Sekunden erledigt:

import Mathlib
-- The sum of two even natural numbers is even.
theorem even_add_even {a b : ℕ} (ha : Even a) (hb : Even b) : Even (a + b) := by
rcases ha with ⟨k, rfl⟩   -- a = k + k for some k
rcases hb with ⟨l, rfl⟩   -- b = l + l for some l
exact ⟨k + l, by ring⟩    -- witness k + l; ring closes the algebra

Beachte, was das Beispiel über die Arbeitsteilung zeigt. Der kreative Schritt ist die Wahl des Zeugen k + l; der prüfende Schritt ist ring, das die Algebra verifiziert. Menschen und Modelle sind beim ersten ganz gut. Nur dem Kernel kann man beim zweiten trauen, und er wird nie müde, überfliegt nichts und bewertet nie nach Gefühl. Das glaubwürdigste Element der gesamten Ankündigung ist genau dieses Gatter: die Behauptung, das Physikpapier sei zurückgehalten worden, bis seine Lean-Formalisierung fertig war. Falls diese Darstellung stimmt, funktioniert hier der Workflow genau wie gedacht — die Maschine schlägt vor, die Maschine entscheidet, und die Pressemitteilung wartet ihren Termin ab.

Wo die Vermutungsgenerierung gewinnt

Die Generierung gewinnt überall dort, wo der Suchraum kombinatorisch ist und die Bewertung billig. DeepMinds FunSearch hat die Vorlage bereits 2023 etabliert: Ein Sprachmodell schlägt programmartige Hypothesen vor, ein schneller Evaluator bewertet sie, und eine evolutionäre Schleife behält die besten — ein Aufbau, der neue Konstruktionen für Cap Sets und bessere Heuristiken für Bin Packing hervorbrachte, als Jahrzehnte handgetuntes Feintuning es geschafft hatten. AlphaEvolve trieb dieselbe Idee weiter und sparte unter anderem eine Multiplikation bei einem Algorithmus zur 4×4-Matrixmultiplikation ein, der seit Strassens Zeiten gestanden hatte. Niemand behauptet, diese Systeme verstünden Geometrie. Das müssen sie auch nicht. Sie müssen vorschlagen, und der Evaluator muss ehrlich sein.

Der ETH-Algorithmus passt beinahe verdächtig gut in dieses Muster. Der Raum der „algorithmischen Ideen“ ist riesig, und menschliche Forschende erkunden ihn mit starken Vorannahmen — was höflich gesagt heißt: mit blinden Flecken. Eine Konstruktion, die einen bestimmten Repräsentationstrick mit einer bestimmten Rekursionsstruktur kombiniert, kann dreißig Jahre unerforscht bleiben, schlicht weil der Suchpfad von niemandem dort vorbeiführte. Erschöpfende, voraussetzungsfreie, leicht stumpfsinnige Suche ist genau das, was Maschinen mitbringen. Dieselbe Logik steckt in Erzeugen-und-Widerlegen-Schleifen: eine Vermutung vorschlagen, sofort versuchen, sie mit einer Suche nach Gegenbeispielen in kleinen Fällen zu Fall zu bringen. Die meisten Vermutungen sterben innerhalb von Minuten, und das ist in Ordnung — jede Widerlegung schärft den nächsten Vorschlag, und die Überlebenden sind jene, die den Nachmittag eines Menschen wert sind.

Es gibt außerdem eine psychologische Asymmetrie, die man respektieren sollte. Wang und Zahls dreidimensionaler Kakeya-Beweis kostete jahrelange konzentrierte Arbeit an der Spitze des Fachs. Wenn eine modellgestützte Suche tatsächlich einen Beweis für alle Dimensionen hervorgebracht hat, dann hat sie mit ziemlicher Sicherheit einen anderen Weg durch die Landschaft gefunden — nicht unbedingt einen tieferen, aber einen anderen. Anderssein ist genau der Zweck der Suche. Die Gefahr besteht nicht darin, dass Maschinen Vermutungen erzeugen, sondern darin, dass jemand eine erzeugte Vermutung veröffentlicht, ohne die Maschinerie, die sie stützt. Damit kommen wir zu dem Teil der Pipeline, den man tatsächlich bauen muss.

Ein Verifikationsworkflow für KI-generierte Beweise

Wer die Vorteile maschinell erzeugter Mathematik ohne die Peinlichkeit will, für den zählt der Workflow mehr als das Modell. Diese Pipeline würde ich in dieser Reihenfolge fahren:

1. Breit und günstig generieren. In dieser Phase schlägt Vielfalt Tiefe; man will Abdeckung des Ideenraums, nicht einen polierten Versuch.
2. Gegen die Literatur deduplizieren. Retrieval über arXiv und MathOverflow fängt den häufigsten Fehler ab: eine „neue“ Vermutung, die ein bekanntes Ergebnis in ungewohnter Notation ist.
3. Günstige empirische Filter anwenden. Kleine Fälle numerisch testen, Gegenbeispiele rechnerisch jagen und die offensichtlich falschen Aussagen schnell sterben lassen.
4. Die Überlebenden formalisieren. Lean, Isabelle oder Rocq — wähle deinen Beweisassistenten, aber verstehe, dass dies der teure Schritt ist und ein Beweis in natürlicher Sprache eine Skizze ist, kein Ergebnis.
5. Menschliche Prüfung auf Neuheit und Einordnung. Ist das wichtig? Ist die Aussage überhaupt die richtige? Modelle optimieren darauf, was beweisbar ist; Menschen entscheiden, was es wert ist, bewiesen zu werden.

Die angekündigte Zusammenarbeit folgte ungefähr dieser Form — Forschende wurden vor der Veröffentlichung eingebunden und übernahmen praktisch Schritt fünf. Das ist eine echte Verbesserung gegenüber dem alten Vorgehen, ein Preprint fallen zu lassen und die sozialen Medien es begutachten zu lassen. Doch beachte die Asymmetrie in der Pipeline: Die Schritte eins bis drei sind billig und skalieren mit der Rechenleistung, Schritt vier ist der Engpass, und Schritt fünf skaliert überhaupt nicht. Wer in diesem Bereich Werkzeuge baut, sollte sein Geld in den Engpass stecken — bessere Autoformalisierung, bessere Fehlerrückmeldung an den Generator — und nicht in einen größeren, selbstbewussteren Generator.

Warum menschliche Mathematiker die Korrektheit weiterhin bewachen

Kein Verifikationsprogramm kann dir sagen, dass ein Satz wichtig ist. Die Auswahl von Problemen ist Geschmackssache, und Geschmack ist eine soziale Technologie, die über Jahrzehnte aufgebaut wurde — Seminare, Gutachten, der langsame Konsens darüber, welche Fragen Türen öffnen und welche Sackgassen sind. Die Skepsis der Forschungsgemeinschaft gegenüber Herstellerankündigungen ist nicht bloß Torwächterei um ihrer selbst willen; sie ist ein Immunsystem, und Immunsysteme reagieren gelegentlich über, gerade weil Unterreaktion tödlich wäre.

Dann ist da noch die Herkunft. Diese Modelle wurden mit den eigenen Fragen, Entwürfen und Forenbeiträgen der Community trainiert, was die unbequeme Möglichkeit aufwirft, dass eine gefeierte „Entdeckung“ eine Neukombination von Dingen ist, die die späteren Gutachter selbst geschrieben haben. Die Angst, das eigene Werkzeug zu überholen, ist keine Paranoia — sie ist ein Problem der Datenherkunft, und solange Labore keine Herkunft nachweisen können, sind menschliche Gutachter die einzigen Plagiatsdetektoren, die funktionieren. Hinzu kommt die Politik der Anerkennung — wer zur Verifikation eingeladen wird, wessen Namen in der Ankündigung stehen, Vorwürfe der Vetternwirtschaft —, und man sieht, warum das menschliche Gatter nicht entfernbar ist. Fünf namhafte Wissenschaftler auszuwählen, die ein Ergebnis absegnen, ist ebenso ein politischer Akt wie ein epistemischer.

Noch eine Warnung für alle, die versucht sind, Bestenlisten als Maß für Forschungsfähigkeit zu lesen: Goldmedaillen bei Wettbewerben messen Leistung bei Aufgaben, die so konstruiert sind, dass sie in Stunden lösbar sind. Forschung ist die genaue Gegenverteilung — Probleme, die gerade deshalb ausgewählt werden, weil niemand weiß, ob sie überhaupt lösbar sind. Aus demselben Grund verfehlen Benchmarks den größten Teil der realen Arbeit beim Software-Engineering: Die Metrik belohnt das zurechtgeschnittene Problem, nicht das unordentliche. Ein Modell, das Olympiadeaufgaben meistert, hat etwas Reales gezeigt. Es hat jedoch kein Urteilsvermögen gezeigt.

Die Empfehlung: Der Schleife vertrauen, nicht dem Modell

Hier meine Position, klar formuliert. Vermutungsgenerierung ist real, nützlich und wird nur besser werden; ungeprüfte Vermutungsgenerierung ist dagegen wertlos, und Beweise in natürlicher Sprache ohne formale Absicherung sollten bis zum Beweis des Gegenteils als Marketing behandelt werden. Beweisprüfung gewinnt immer dann, wenn das Artefakt geglaubt werden muss. Generierung gewinnt immer dann, wenn der Engpass Vorstellungskraft statt Strenge ist. Die Ankündigungen, auf die es ankommt, sind jene, in denen beide miteinander verschraubt sind.

Behandle das Modell also wie einen produktiven jungen Mitarbeiter mit unendlicher Energie und ohne Urteilsvermögen: Alles, was er dir liefert, geht durch den Beweisassistenten, bevor es in das Paper kommt, und durch einen Menschen mit Geschmack, bevor es in die Einleitung kommt. Bist du Forscher, lerne einen Beweisassistenten richtig — Formalisierung ist der Engpass, und wer sie beherrscht, wird bald sehr gefragt sein. Baust du Werkzeuge, bau die Schleife, nicht die Demo. Und wenn die nächste große Ankündigung kommt, überspringe die Pressemitteilung, öffne das Preprint und prüfe, ob das Lean-Repository existiert. Die Behauptungen, die überleben, sind jene, die bereits maschinell geprüft ankommen.