Kann KI Mathe? Drei Stufen und die Frage, wer es prüft

Wer KI im Alltag nutzt, kennt den Widerspruch: Ein Chatbot verrechnet sich manchmal bei einer langen Kassenbon-Summe, während gleichzeitig Schlagzeilen melden, dass neue Modelle schwere Mathematik-Wettbewerbe lösen oder bei Forschungsproblemen helfen.

Die Auflösung liegt darin, dass „Kann KI Mathe?“ drei ganz unterschiedliche Aufgaben vermischt: Alltagsrechnen, Wettbewerbsaufgaben mit vielen Zwischenschritten und mathematische Beweise für unendlich viele Fälle.

Ein reines Sprachmodell ist zunächst kein Taschenrechner: Es sagt Schritt für Schritt das nächste wahrscheinliche Wort- oder Zahlenteil voraus (Stufe 1). Bei langen Zahlenketten ohne Hilfsmittel kann eine einzige falsch fortgesetzte Ziffer das Ergebnis kippen. Sobald das System die Rechnung dagegen an ein Code-Werkzeug (z. B. Python) übergibt, rechnet ein exakter Programmierkern und gibt das Ergebnis zurück.

Auf Stufe 2 (Wettbewerbsaufgaben wie AIME 2025 oder FrontierMath) reicht eine einzelne Formel nicht. Neuere Reasoning-Modelle zerlegen das Problem vor der Antwort in Zwischenschritte, probieren Ansätze aus und verwerfen Sackgassen. Während Modelle bei AIME 2025 inzwischen sehr hohe Trefferquoten erreichen, zeigt FrontierMath mit seinen Stufen 1 bis 4, dass auf Forschungsniveau weiterhin viele Aufgaben ungelöst bleiben.

• Epoch AI: FrontierMath Benchmark
• Epoch AI: FrontierMath Tier 4

In der höheren Mathematik geht es selten um eine einzelne Zahl, sondern um Aussagen über unendlich viele Zahlen. Ein klassisches Lehrbeispiel zeigt, warum Ausprobieren dafür nicht genügt:

Betrachte die Formel n² + n + 41 für nichtnegative ganze Zahlen n:

• Für n = 0 ergibt sich 41 (Primzahl).
• Für n = 1 ergibt sich 43 (Primzahl).
• Für n = 2 ergibt sich 47 (Primzahl).

Auch für n = 3 bis n = 39 liefert die Formel ausschließlich Primzahlen. Trotzdem ist die Aussage „Die Formel liefert immer eine Primzahl“ falsch: Für n = 40 steht dort 40² + 40 + 41 = 1.681 = 41 × 41. Ein einziges Gegenbeispiel widerlegt vierzig erfolgreiche Tests.

Anders ist es bei der Aussage: Der Unterschied zweier aufeinanderfolgender Quadratzahlen ist immer ungerade. Hier liefert die Umformung (n + 1)² − n² = n² + 2n + 1 − n² = 2n + 1 einen allgemeinen Beweis für alle ganzen Zahlen n, weil 2n immer gerade und 2n + 1 immer ungerade ist.

Wenn KI-Systeme wie AlphaProof oder Forschungsmodelle an neuen mathematischen Beweisen arbeiten (etwa bei OpenAIs veröffentlichter Arbeit zu einer Variante des Navier-Stokes-Problems mit glatter äußerer Kraft vom September 2026), stellt sich eine entscheidende Frage: Wer prüft eigentlich einen seitenlangen, plausibel klingenden Beweistext?

Hier hilft ein formaler Beweisassistent wie Lean:

• Wofür er gebraucht wird: Um mathematische Aussagen und Beweise lückenlos nach strengen logischen Regeln zu kontrollieren.
• Was er bekommt: Die exakten Definitionen, Voraussetzungen, die Behauptung und jeden einzelnen Beweisschritt in formaler Sprache.
• Was er tut: Sein kleiner Prüfkern kontrolliert Schritt für Schritt, ob jede Umformung erlaubt ist und keine Voraussetzung fehlt.
• Was herauskommt: Ein formal bestätigter Beweis oder die exakte Zeile, an der ein Schluss noch nicht trägt.

Menschen müssen dabei weiterhin prüfen, ob die formal aufgeschriebene Behauptung wirklich die gemeinte Frage ausdrückt und welche Zusatzbedingungen gelten.

• Lean 4: Theorem Proving in Lean
• Google DeepMind: AlphaProof and AlphaGeometry 2
• OpenAI: Navier-Stokes Solution (September 2026)
• OpenAI: Sharing AI Progress in Mathematics (Oktober 2026)