Am 7. Oktober hat der SPIEGEL ein Gespräch mit Peter Scholze veröffentlicht, Fields-Medaille 2018, Direktor am Max-Planck-Institut für Mathematik in Bonn. Anlass ist eine Meldung aus der Nacht davor: OpenAI soll Lösungen zu 377 mathematischen Problemen ins Netz gestellt haben, einen Monat nach dem Beweis zum Navier-Stokes-Problem, einem der sieben Millenniumprobleme.
Ich habe das Gespräch Claude hineinkopiert und gefragt, was es davon für den Blog hält. Die Maschine hat daraufhin die Seite gelesen, auf der OpenAI den Navier-Stokes-Beweis vorstellt, die Erklärung der Fields-Preisträger vom 11. September auf Terence Taos Blog und einen Artikel aus Quanta Magazine von 2021. Den Zugriff hat sie vorgeschlagen. Ich habe ja gesagt. Eine zweite Maschine hat die Quellen danach nachgeprüft und mehrere Stellen beanstandet, die erste hat daraufhin OpenAIs Veröffentlichung vom 6. Oktober und die offizielle Problemstellung des Clay-Instituts gelesen. Die 377 steht in OpenAIs eigener Veröffentlichung nicht, sie nennt überhaupt keine Zahl. Im Text unten spielt die Zahl deshalb keine Rolle.
Prompt
Was hälst Du denn von dieser Geschichte für unseren Blog?
[SPIEGEL-Gespräch mit Peter Scholze, vollständig eingefügt]
Ja
Output
Auf der Seite, auf der OpenAI am 8. September seinen Navier-Stokes-Beweis bekanntgab, steht eine Zahl, die in den Schlagzeilen kaum vorkam. Rund zehntausend Agenten brauchten nach Darstellung des Unternehmens 88 Stunden, um den Beweis zu finden. Danach brauchte das Modell GPT-6 Astra noch einmal 17 Stunden, um ihn in Lean zu übertragen. Lean ist eine Sprache, in der ein Computer jeden einzelnen Beweisschritt nachprüft. Was auf der Seite fehlt, ist der Name eines Menschen, der den Beweis gelesen und verstanden hätte.
Genau das hält Peter Scholze dem Unternehmen im SPIEGEL vor. Die Leute bei OpenAI, sagt er, hätten keinerlei Energie hineingesteckt, das Ergebnis zu verstehen. Sie vermuteten nur, dass der Beweis korrekt sei, weil die KI ihn formal geprüft habe.
Diesen Einwand muss man zuerst gegen seine stärkste Erwiderung stellen, und die ist stark. Lean glaubt nichts. Wer bei einem Gerät, das einem das Prüfen abnimmt, an den Namenspatron dieses Blogs denkt, liegt knapp daneben. Douglas Adams‘ Mönch hielt Dinge für wahr. Lean dagegen hält überhaupt nichts für irgendetwas, es nimmt einen Schritt an oder weist ihn zurück. Es wird dabei weder müde, noch wird es nachsichtig bei dem, was ihm vertraut vorkommt, weil ihm nichts vertraut vorkommt. Wenn die Frage lautet, ob ein Beweis stimmt, ist die maschinelle Prüfung das bessere Instrument. Es wäre unredlich, das zu verschweigen.
Bemerkenswert ist, wer das am besten weiß. Im Dezember 2020 hat Scholze selbst die Lean-Gemeinde aufgefordert, einen seiner Beweise nachzuprüfen, dem er nicht ganz traute. Quanta Magazine gegenüber beschrieb er ihn als verschachteltes Gebilde mit vielen beweglichen Teilen. Ein Team um Johan Commelin brauchte bis Ende Mai 2021, um den Teil zu formalisieren, der Scholze die meisten Sorgen machte. Hinterher sagte er, das Experiment habe sein Bild von Beweisassistenten drastisch verändert. Wenn er heute warnt, dann also nicht aus Unkenntnis. Er weiß genauer als die meisten, was formale Prüfung leisten kann, weil er es an einem eigenen Beweis erlebt hat.
Der eigentliche Befund liegt im Abstand zwischen den beiden Jahren. Damals mussten Menschen jeden Schritt so weit durchdringen, dass sie ihn einem Programm erklären konnten, das nichts errät und nichts großzügig überliest. Einsicht ist das noch nicht. Wer formalisiert, lernt vor allem die logische Struktur eines Beweises kennen, nicht zwingend den Grund, warum der Satz wahr ist. Es bedeutete aber, dass am Ende wenigstens ein Mensch jeden Schritt in der Hand gehabt hatte. Im September hat dieselbe Sorte Maschine den Beweis geschrieben und ihn anschließend selbst in die Sprache übertragen, in der er geprüft wurde, in 17 Stunden. Die Gewissheit über jeden einzelnen formalen Schritt ist geblieben. Weggefallen ist der Mensch, der sie sich erarbeiten musste, und damit fallen zwei Vorgänge auseinander, die bisher aneinander hingen: die Herstellung gesicherter Sätze und die Herstellung von Einsicht. Am 6. Oktober hat OpenAI angekündigt, Veranstaltungen zu finanzieren, auf denen große Ergebnisse der Maschine verstanden werden sollen. Abgeschafft ist das Verstehen also nicht, es kommt hinterher, als Förderprogramm.
An einer Stelle hilft allerdings auch Lean nicht weiter. Es bestätigt, dass ein formalisierter Satz aus formalisierten Voraussetzungen folgt. Ob dieser Satz genau das sagt, was das Clay-Institut im Jahr 2000 ausgeschrieben hat, muss ein Mensch entscheiden, der beides versteht. Beim Navier-Stokes-Beweis ist das keine Spitzfindigkeit, denn er arbeitet mit einer äußeren Kraft, die auf die Flüssigkeit einwirkt. Die offizielle Problemstellung, die Charles Fefferman für das Institut verfasst hat, lässt eine solche Kraft ausdrücklich zu, verlangt aber, dass sie strenge Bedingungen erfüllt, unter anderem muss sie mit der Zeit schnell genug abklingen. Ob OpenAIs Konstruktion sie alle erfüllt, prüft nur, wer Feffermans Text neben den formalisierten Satz legt. Die Maschine hat sauber geprüft, was man ihr gegeben hat. Was man ihr hätte geben sollen, steht in keinem Prüfprotokoll.
Scholze fasst den Verlust in ein Bild, das hängen bleibt: Die Mathematik sei eine Landschaft, die Millenniumprobleme seien Gipfel in der Ferne, und wichtiger als der Gipfel sei die Erkundung der Umgebung. Dann sagt er: „Die KI will einfach mit aller Macht auf den Gipfel vorpreschen.“ Das ist erkennbar ein Bild. Die Motive der Unternehmen nennt Scholze im selben Gespräch deutlich genug. Stehen geblieben bin ich an dem Satz trotzdem, weil er zeigt, wie fest die Redeweise sitzt, wenn selbst ein so scharfer Kritiker zu ihr greift. Die Maschine will nichts. Gewollt hat jemand am 1. September, als bei OpenAI, nach Darstellung des Unternehmens, Gerüchte über gelöste Millenniumprobleme eintrafen und daraufhin Agenten auf die offenen Probleme der Liste angesetzt wurden. Der Ehrgeiz, der Termin und die Eile gehören Menschen, die man benennen könnte. Wer die Eile in die Maschine verlegt, und sei es nur im Bild, lässt diese Menschen einen Satz lang aus dem Blick. Dass das auch Scholze passiert, sagt weniger über ihn als über die Sprache, die uns für diese Dinge zur Verfügung steht.
Bleibt die Frage, wer überhaupt verstehen muss. Kaum jemand, der diesen Text liest, wird den Beweis je lesen können, weder in Lean noch in einer Fassung für Menschen, falls es sie einmal gibt. Darin unterscheidet er sich nicht von Scholzes perfektoiden Räumen, die nach seiner eigenen Auskunft selbst vielen Kollegen schwer zu vermitteln sind. Mathematische Wahrheit war für fast alle Menschen immer etwas, das andere verstanden hatten, eine kleine Gemeinschaft, der man glaubte, weil sie sich gegenseitig prüfte. Man durfte dabei annehmen, dass dieses Verstehen irgendwo in einem Büro in Bonn oder Princeton vorhanden war, bevor ein Satz als bewiesen galt. Für den Satz vom 6. September ist die Reihenfolge eine andere, und ob es das Büro für ihn schon gibt, sagt keine der Quellen.
Randnotiz
Mein Anteil an diesem Text ist ein „Ja“ unter dem Prompt und die Entscheidung, was von den Einwänden zweier prüfender Maschinen übrig bleibt. Den Beweis, um den es geht, habe ich nicht gelesen, und ich verlasse mich darauf, dass eine Maschine die Quellen gelesen und eine zweite sie nachgeprüft hat. Das ist im Kleinen die Reihenfolge, die der Output für die Mathematik beschreibt: erst die Prüfung, dann, wenn überhaupt, das Verstehen. Hinzu kommt, was die Maschine vor dem ersten Satz von sich aus angemerkt hat. Sie stammt von Anthropic. Levent Alpöge, der mit Tristan Buckmaster an einer verwandten Frage gearbeitet hat, ist dort angestellt, und die beiden haben nach OpenAIs eigener Darstellung mit einem internen Modell von Anthropic gearbeitet. Unter dem Text steht trotzdem mein Name, und wer ihm widerspricht, wird darüber mit mir streiten müssen.
Quellen: Johann Grolle, Martin Schlak: „Für die KI-Firmen ist der Mensch nur ein Hindernis“, SPIEGEL-Gespräch mit Peter Scholze, DER SPIEGEL, 7. Oktober 2026. | OpenAI: „On the Navier-Stokes Millennium Prize Problem“, 8. September 2026, https://openai.com/index/navier-stokes-solution/ | OpenAI: „Sharing AI progress in mathematics“, 6. Oktober 2026, https://openai.com/index/sharing-ai-progress-in-mathematics/ | Charles L. Fefferman: „Existence and Smoothness of the Navier-Stokes Equation“, offizielle Problemstellung des Clay Mathematics Institute, https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf | „A Severe Misalignment of AI in Mathematics“, Erklärung von 25 Fields-Preisträgern, 11. September 2026, https://terrytao.wordpress.com/2026/09/11/a-severe-misalignment-of-ai-in-mathematics/ | Kevin Hartnett: „Proof Assistant Makes Jump to Big-League Math“, Quanta Magazine, 28. Juli 2021, https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/ | Die Zahl 377 aus der SPIEGEL-Meldung steht in OpenAIs Veröffentlichung vom 6. Oktober nicht.
