Es ist eines der seltsamsten Ergebnisse der Mathematik: Wenn man eine Kugel in winzige Bestandteile zerlegt und dann wieder zusammensetzt, hat man zwei neue Kugeln, die beide genauso groß sind wie die ursprüngliche Kugel. Dieser »Satz von Banach-Tarski« erlaubt es also, Kugeln wie auf magische Weise zu verdoppeln - und ist daher einigen Fachleute ein Dorn im Auge. Doch wie sich herausstellt, lässt sich dieses Paradoxon vermeiden. Ein fast vergessener Ansatz aus den 1990er Jahren soll das bewerkstelligen. Nun haben eine Schülerin und ein Schüler diesen im Detail untersucht und mit Hilfe eines Computers überprüft.

Schon seit der Veröffentlichung von Stefan Banach und Alfred Tarski im Jahr 1924 sorgt die seltsame Verdopplung für Unmut in der Mathematik. Einige Fachleute sahen das Ergebnis als Hinweis darauf, dass eine der Grundannahmen, auf denen das gesamte Fach fußt, falsch sein muss. Denn möglich wird das Paradoxon nur durch das sogenannte Auswahlaxiom, das es erlaubt, aus einer Reihe von Mengen je ein Element auszuwählen. Anfang des 20. Jahrhunderts forderten einige Kritiker daher, das Auswahlaxiom aus den mathematischen Grundannahmen zu entfernen. Wie sich aber zeigt, tauchen durch das fehlende Auswahlaxiom noch seltsamere Ergebnisse auf - Weglassen ist für die meisten Mathematikerinnen und Mathematiker also keine Option.

Und dann gelang dem französischen Forscher Olivier Leroy in den 1990er Jahren das Unmögliche: Er konnte das Banach-Tarski-Paradoxon aushebeln, ohne auf das Auswahlaxiom verzichten zu müssen. Er hielt seine Gedanken dazu in Notizen fest, doch bevor er sie ordnen und veröffentlichen konnte, verstarb er im Jahr 1996 unerwartet. 17 Jahre später fassten zwei ehemalige Kollegen seine Dokumente in einer 40-seitigen französischsprachigen Arbeit zusammen, die sie online zur Verfügung stellten. Leroy erweiterte demnach das Fachgebiet der Topologie, einer abstrakteren Form der Geometrie. Indem der Mathematiker die Bedingung wegließ, dass sich die Topologie mit Punkten befassen müsse, konnte er viele der etablierten Konzepte des Fachs erweitern. Unter anderem ließ sich damit beweisen, dass das Banach-Tarski-Paradoxon verschwindet: Eine Kugel lässt sich in dieser neuen Topologie nicht mehr verdoppeln - und das, obwohl das Auswahlaxiom noch immer gilt.

Ein Beweisprüfer für eine kaum bekannte Arbeit

Dieser Beweis, der bis in die abstraktesten Tiefen der Mathematik reicht, hat es den beiden Abiturienten Chiara Cimino und Christian Krause angetan. Krause beschäftigt sich seit mehreren Jahren mit verschiedenen Programmiersprachen und nahm in der Vergangenheit an Jugend-forscht-Wettbewerben teil. Dort lernte er Cimino kennen, deren Themenschwerpunkt in der Mathematik liegt. Seit 2020 studiert sie neben der Schule Mathematik an der Universität Konstanz und hat dort schon sieben Semester absolviert.

Im Jahr 2023 beschlossen die beiden Schüler schließlich, ein gemeinsames Projekt zu starten. Sie wollten einen mathematischen Beweis »formalisieren«: ihn also in eine für Computer verständliche Programmiersprache übersetzen und prüfen lassen. Letzteres macht ein Beweisprüfer, ein Computerprogramm, das die logische Abfolge von Aussagen durchgeht und auf Widersprüche prüft. Das ist ein ziemlich aufwändiges Unterfangen: Oft sind professionelle Mathematiker tage-, wochen- oder gar monatelang damit beschäftigt, einen Beweis zuerst in die passende Form zu bringen und ihn dann in die Programmiersprache Lean zu übersetzen, damit ein Computer ihn verarbeiten kann. »Ich sollte mich der Mathematik widmen und Christian dem Informatikteil«, sagt Cimino. »Aber wie sich herausstellte, lassen sich die beiden Teile nicht voneinander trennen.«

Cimino und Krause teilten den Beweis in Leroys französischem Paper zunächst in einem »Blueprint« in dutzende Teilschritte auf: Sie mussten bestimmte Größen definieren, kleinere Beweise führen und alles am Ende zu einem Gesamtergebnis verbinden. Dabei mussten sie den Beweis an einigen Stellen nachfüttern, denn unter anderem enthielt er Passagen, in denen ein Schritt als »trivial« dargestellt und nicht weiter ausgeführt wurde. »Das hat dann teilweise mehrere hundert Zeilen an Code erfordert«, sagt Krause. Doch nach fast zwei Jahren Arbeit, an denen sie sich regelmäßig an den Wochenenden im Schülerforschungszentrum trafen, haben sie es geschafft: Cimino und Krause haben den Beweis von Leroy formalisiert und überprüft und ergatterten mit dieser Leistung den zweiten Platz beim Jugend-forscht-Wettbewerb des Jahres 2025.

Damit haben sie auch einen wichtigen Beitrag für die Mathematik-Community geleistet. Derzeit arbeiten viele Fachleute daran, die Datenbanken von Beweisprüfern um grundlegende Definitionen und Beweise zu erweitern. Ziel ist es, dass sich irgendwann jeder mathematische Beweis mit einem Computer überprüfen lässt. Dazu ist aber viel Vorarbeit nötig. Im Prinzip muss das gesamte mathematische Wissen in Programmiersprache übersetzt werden. Cimino und Krause haben nun einige wichtige Beiträge geliefert: Viele Definitionen, Sätze und Beweise aus der Topologie, die sie formalisiert haben, sind jetzt für Forscherinnen und Forscher weltweit abrufbar.

Die beiden Preisträger haben mittlerweile die Schule beendet und beginnen beide ein Studium. Cimino widmet sich in Bonn weiterhin der Mathematik, während Krause in Heidelberg Physik studieren möchte. Doch für beide steht fest: Sie wollen sich weiterhin mit Beweisprüfern beschäftigen.