Fields-Medaillen warnen: Mathematik und KI-Firmen verfolgen verschiedene Ziele

Die Spannung zwischen der mathematischen Gemeinschaft und den Unternehmen, die künstliche Intelligenz entwickeln, ist keine Hinterzimmerdebatte mehr. In „Le Monde“ erschien ein Text, den fünfundzwanzig Träger der Fields-Medaille unterzeichnet haben, der höchsten Auszeichnung der Mathematik. Darin schreiben die Autoren, dass die Ziele der KI-Firmen und die Ziele der mathematischen Gemeinschaft weit auseinandergehen. Der Vorwurf richtet sich nicht dagegen, dass Modelle Aufgaben lösen. Er richtet sich dagegen, wozu man sie löst und wie darüber gesprochen wird.

Ein Beweis ist kein Produkt

Wenige Tage später veröffentlichte „Le Monde“ ein Gespräch mit Stéphane Mallat, Mathematiker an der ENS, 2025 mit der Goldmedaille des CNRS geehrt, Mitentwickler des Kompressionsalgorithmus JPEG 2000. Sein Satz steht über der ganzen Debatte: Von KI erzeugte Beweise sind für sich genommen wenig wert, wenn wir nicht genügend Vorbereitung haben, um sie zu verstehen. Mallat befasst sich unter anderem mit dem Fluch der Dimensionen. Bei diesem Problem wächst die Zahl möglicher Konfigurationen so stark, dass es keinen Sinn mehr ergibt, Intuition aus niedrigen Dimensionen zu gewinnen.

Das Argument lässt sich konkret fassen. Mathematik ist nicht nur eine Menge wahrer Sätze. Sie ist auch eine Technik zu verstehen, warum sie wahr sind. Ein Prüfer bestätigt die Korrektheit einer formalen Notation. Dem Lernenden vermittelt er keine dieser Fähigkeiten, solange sie nicht dargelegt und diskutiert wird.

Was maschinelle Verifikation heute leistet

Parallel entstehen Arbeiten, die zeigen, wie eine solide Zusammenarbeit von Mensch und Maschine aussieht. Mario Carneiro weist in einem Artikel auf arXiv nach, dass in der Typentheorie des Assistenten Lean der Satz vom ausgeschlossenen Dritten genügt, ohne Auswahlaxiom, ohne Extensionalität der Sätze, ohne Quotienten, um die Widerspruchsfreiheit der Mengenlehre ZF zu beweisen, und zwar in vollständig formalisierter Form. Das ist ein technisches Ergebnis, doch es hat philosophisches Gewicht. Bisher konnte man annehmen, dass ohne den Auswahloperator die Stärke der Typentheorie deutlich unter ZF fällt.

Der zweite Strang ist die verifikationsgestützte Suche. Ein Modell schlägt Programme im FunSearch-Stil vor, ein harter Evaluator bewertet sie, und die Auswahl behält die besten. Die Autoren einer solchen Arbeit führten ein Experiment sogar auf einem Laptop durch, mit einem lokalen Dreißig-Milliarden-Modell und 120 bis 600 verifizierten Proben pro Durchlauf. Das Ergebnis ist zweideutig und gerade deshalb wertvoll. Die Suche stoppte, nachdem sie etwas mehr als 90 Prozent der Lücke zum Rekord bei der Flaggschiff-Aufgabe geschlossen hatte. Als man dem Modell einen Hinweis auf die Familie der Konstruktionen gab, optimierte die Schleife die vorgegebene Idee, obwohl keiner der eigenständigen Durchläufe sie entdeckt hatte.

Im Hintergrund bleibt die Frage der Anreize. Wenn das wichtigste Kriterium ein Rekord in der Tabelle wird, verwandelt sich Mathematik in eine Sammlung von Benchmarks und nicht in eine Praxis des Verstehens. Vorsicht vor einer solchen Vereinfachung ist keine Feindschaft gegenüber Werkzeugen. Sie ist die Bedingung dafür, dass Werkzeuge dauerhaft zu etwas nützlich sind.