Alle Tests grün. Und trotzdem falsch.

1970 stellten Paul Erdős und András Sárközy eine Frage. Sie suchten eine unendliche Menge von Zahlen, in der keine Zahl die Summe zweier grösserer Zahlen aus derselben Menge teilt.

Schon drei Zahlen können die Regel brechen: 3, 4 und 5. Denn 3 teilt 4 + 5. Versuchen Sie jetzt, eine unendliche Menge zu bauen, in der das nie passiert – und die trotzdem gross genug ist, um mathematisch interessant zu sein.

Die Frage blieb 56 Jahre offen. Dann fand AlphaProof Nexus von Google DeepMind einen Beweis.

Wenn mir jemand als CTO sagt: «Unsere KI hat es gelöst», habe ich eine Anschlussfrage: Woher wissen wir das?

Die beeindruckendste Antwort kann falsch sein

KI schreibt heute Code, Analysen und mathematische Argumente in Sekunden. Sie kann auch in Sekunden falschliegen. Bei einem langen Beweis genügt ein einziger unzulässiger Schritt. Der Rest kann brillant sein – das Ergebnis ist trotzdem falsch.

AlphaProof Nexus formuliert seine Beweisversuche deshalb in Lean. Diese Software prüft die mathematischen Schritte. Scheitert einer, muss das System weiterarbeiten.

Dann folgt eine zweite Prüfung: Mathematiker kontrollieren, ob die formal geprüfte Aufgabe tatsächlich der ursprünglichen Frage entspricht. Denn ein perfekter Beweis für die falsche Frage hilft niemandem.

Ich kenne diese Geschichte aus der Softwareentwicklung

Ein KI-Agent soll den Checkout eines Onlineshops ändern: zehn Prozent Rabatt auf den Warenkorb, Geschenkkarten sind ausgenommen. Der Agent schreibt den Code. Alle Tests sind grün. Die Änderung geht live.

Dann kauft jemand eine Geschenkkarte – und bekommt den Rabatt. Der Code bestand jeden Test. In den Tests kam schlicht keine Geschenkkarte vor. Der Fehler lag in der Frage, die wir dem System und seinen Tests gestellt haben.

Genau solche Fragen sind bei uns Forschungsarbeit. Wie erkennt ein System, dass ein Ergebnis zwar plausibel aussieht, aber eine entscheidende Bedingung verfehlt? Wie machen wir Annahmen und Grenzen sichtbar? Und wie lässt sich eine Prüfung so in den Arbeitsablauf einbauen, dass sie tatsächlich genutzt wird?

Was wir dabei lernen, fliesst in unsere Produkte ein. Denn Verlässlichkeit entsteht nicht durch ein Versprechen auf der Website. Sie muss sich in der Nutzung zeigen. Die Mathematiker mussten prüfen, ob ihr System die richtige Frage beantwortet. Wir müssen das bei den Aufgaben schaffen, die Menschen unseren Produkten anvertrauen.

Zeigen Sie mir auch die 344 anderen Versuche

AlphaProof Nexus fand Beweise für neun von 353 untersuchten offenen Erdős-Problemen. Für die übrigen fand es in diesem Versuch keinen.

war die Frage offen

56 Jahre

offenen Erdős-Problemen bewiesen

9 von 353

Versuche ohne Beweis

344

Ich finde diese Zahl grossartig – gerade weil beide Teile sichtbar sind. Neun zeigen das Potenzial. 353 zeigen den Massstab, an dem es gemessen wurde.

So möchte ich KI auch in meinem Unternehmen beurteilen. Ich brauche keine Präsentation mit den fünf schönsten Ergebnissen. Ich will wissen, wo das System scheitert – und ob wir es erkennen, bevor unsere Kunden es tun.

Die Frage der nächsten Jahre ist nicht, wie viele Antworten KI produzieren kann. Die Frage ist, welchen Antworten wir Verantwortung übertragen können.

Daran forschen wir. Und daran müssen sich unsere Produkte messen lassen.