Diese Analyse untersucht Aufgabe 6 der Internationalen Mathematik-Olympiade (IMO) 2025 in Australia sowie den rapide fortschreitenden Wandel in der mathematischen KI-Beweisführung zwischen 2024 und 2026. Bei Aufgabe 6 handelte es sich um ein hochkomplexes kombinatorisches Parkettierungsproblem auf einem $2025 \times 2025$-Gitter, bei dem die minimal erforderliche Anzahl rechteckiger Fliesen unter der Bedingung ermittelt und bewiesen werden musste, dass genau ein unbelegtes Einheitsquadrat ("Lücke") pro Zeile und Spalte verbleibt. Weniger als 1 % der menschlichen Teilnehmer lösten die Aufgabe; KI-Systeme scheiterten 2025 an dieser spezifischen Aufgabe, bevor öffentlich zugängliche Reasoning-Modelle bis 2026 alle sechs IMO-Aufgaben ohne Übersetzung lösen konnten.
Die mathematische Minimallösung nutzt die Symmetrie des Gitters über eine gekippte Windmühlen-Anordnung quadratischer Fliesen der Seitenlänge $k$ auf einem $k^2 \times k^2$-Gitter (für 2025 entspricht dies $k=45$). Der exakte untere Grenzwert der Fliesenanzahl wird durch die Formel $k^2 + 2k - 3$ beschrieben (für $k=45$ ergibt dies exakt 2.112 Fliesen). Der formale Beweis stützt sich auf eine Aufteilung des Gitters in vier Richtungsregionen anhand zweier kreuzender Pfade, die der längsten steigenden Teilfolge (LIS) und der längsten fallenden Teilfolge (LDS) der Lücken-Permutation entsprechen. Unter Anwendung des Erdős-Szekeres-Theorems ($LIS \cdot LDS \ge k^2$) und der Ungleichung vom arithmetischen und geometrischen Mittel (AM-GM) wird bewiesen, dass keine gültige Konfiguration mit weniger Fliesen existieren kann. Der Fall verdeutlicht zudem eine fundamentale Transformation der Mathematik: Während KIs reine formal-logische Beweise automatisieren, gewinnt das Erstellen „motivierter Erklärungen“ zur Förderung des menschlichen Begreifens an zentraler akademischer Bedeutung.
Wichtigste Punkte & Zeitstempel
00:03 IMO 2025 Problem 6: Über 600 Schüler konkurrierten in Australien an sechs Aufgaben; weniger als 1 % erzielten die volle Punktezahl bei Aufgabe 6, der letzten IMO-Aufgabe, die von KI-Systemen im Jahr 2025 nicht gelöst werden konnte.
01:39 Evolution der KI-Leistung: Während DeepMinds AlphaProof 2024 noch eine Übersetzung der Aufgaben in die Formalsprache Lean benötigte, lösten KIs 2025 bereits 5 von 6 Aufgaben direkt und erreichten bis 2026 über kommerziell verfügbare Reasoning-Modelle volle Punktzahlen.
04:11 Problemstellung und Parkettierungs-Regeln: Auf einem $2025 \times 2025$-Gitter müssen überschneidungsfreie Rechtecke so platziert werden, dass in jeder Zeile und jeder Spalte exakt ein unbelegtes Einheitsquadrat (Lücke) verbleibt.
07:34 Das Würfelschnitt-Rätsel als Beweis-Analogie: Das Zerlegen eines $3 \times 3 \times 3$-Würfels in 27 Einheitswürfel erfordert mindestens 6 Schnitte, da die 6 Innenflächen des zentralen Würfels jeweils einen isolierten Schnitt erzwingen – eine Analogie zur Notwendigkeit von Untergrenzen-Beweisen über Randbeziehungen.
11:08 Kanten-Zuordnung und Effizienz-Kriterium: Jede Fliese kann maximal 4 Kanten der Lücken-Quadrate abdecken; eine optimale Parkettierung maximiert die Zahl der Fliesen, die genau 4 Lücken an ihren Ecken berühren.
15:40 Windmühlen-Konstruktion und Formel: Für ein $k^2 \times k^2$-Gitter liefert eine Windmühlen-Anordnung aus $k \times k$-Quadraten die minimale Fliesenanzahl von $k^2 + 2k - 3$ (für $k=45$, also das $2025 \times 2025$-Gitter, entspricht dies 2.112 Fliesen).
24:43 Regionen-Aufteilung durch Pfade: Zur Beweisführung wird das Gitter durch zwei Pfade über die Lücken in vier Quadranten unterteilt, wodurch Kanten eindeutig einzelnen Fliesen ohne Doppelzählung zugeordnet werden.
31:33 Permutationen und Subsequenzen: Die Anordnung der Lücken entspricht einer mathematischen Permutation der Zahlen $1$ bis $k^2$, wobei die Pfade der längsten steigenden Teilfolge ($LIS$) und der längsten fallenden Teilfolge ($LDS$) entsprechen.
39:56 Erdős-Szekeres-Theorem und AM-GM-Ungleichung: Das Erdős-Szekeres-Theorem garantiert $LIS \cdot LDS \ge k^2$. Die AM-GM-Ungleichung zeigt, dass $\frac{LIS + LDS}{2} \ge \sqrt{LIS \cdot LDS} \ge k$, womit der untere Schwellenwert von $2k$ mathematisch streng bewiesen ist.
46:01 Motivierte Erklärungen vs. KI-Beweisgenerierung: Da KI-Systeme formale Beweise ohne menschliches Verständnis generieren können, verschiebt sich der Fokus der Mathematik von der reinen Beweisfindung hin zur Erschaffung „motivierter Erklärungen“, die das menschliche Denken erweitern.
Diskussions-Highlights
Mangel an Geduld bei KI-Systemen: Thang Luong (Research Director bei Google DeepMind) betonte, dass KI-Systemen im Jahr 2025 die Fähigkeit fehlte, „geduldig“ zu sein. Das Modell versuchte sofortige Lösungswege zu generieren, statt ein tiefes, exploratives Verständnis für die Struktur des Problems zu entwickeln.
Wandel des AGI-Benchmarks: Während 2023 Gold-Medaillen bei der IMO noch als Maßstab für eine allgemeine künstliche Intelligenz (AGI) galten, wurden IMO-Probleme bis 2026 im Eiltempo durch fortgeschrittene Reasoning-Modelle kompromittiert, was die Testdomäne in den Bereich der echten mathematischen Forschung verschob.
Bedeutung von „Motivierten Erklärungen“: Das bloße Vorhandensein eines formalen Beweises (wie ihn ein automatischer Theorembeweiser ausgibt) gestiftet keinen epistemischen Mehrwert für den Menschen. Die mathematische Praxis muss die pädagogisch-strukturelle Herleitung („motivierte Erklärung“) als eigenständige akademische Leistung anerkennen.
Glossar
IMO (Internationale Mathematik-Olympiade): Der weltweit prestigeträchtigste Schülerwettbewerb im Bereich der theoretischen Mathematik.
Lean: Ein formaler Theorembeweiser und eine funktionale Programmiersprache, die verwendet wird, um mathematische Beweise auf exakte algorithmische Korrektheit zu prüfen.
AlphaProof: Ein von Google DeepMind entwickeltes KI-System, das über Reinforcement Learning und formale Sprachen (Lean) mathematische Sätze beweist.
Permutation: Eine bijektive Abbildung einer endlichen Menge auf sich selbst; im Kontext des Problems die Anordnung der $N$ Lücken über die $N$ Zeilen und Spalten.
LIS (Longest Increasing Subsequence): Die längste monoton steigende Teilfolge innerhalb einer gegebenen Permutation.
LDS (Longest Decreasing Subsequence): Die längste monoton fallende Teilfolge innerhalb einer gegebenen Permutation.
Erdős-Szekeres-Theorem: Ein zentraler Satz der Kombinatorik, der besagt, dass jede Permutation der Länge $n$ mindestens eine steigende Teilfolge der Länge $a$ oder eine fallende Teilfolge der Länge $b$ enthält, sodass $a \cdot b \ge n$.
AM-GM-Ungleichung (Ungleichung vom arithmetischen und geometrischen Mittel): Eine fundamentale mathematische Ungleichung, die besagt, dass das arithmetische Mittel reeller Zahlen stets größer oder gleich ihrem geometrischen Mittel ist ($\frac{a+b}{2} \ge \sqrt{ab}$).
AGI (Artificial General Intelligence): Eine hypothetische KI, die menschliche kognitive Fähigkeiten über sämtliche intellektuelle Domänen hinweg erreicht oder übertrifft.