LEAN, Logik, Lokale: Banach-Tarski im Licht moderner Mathematik!

LEAN, Logik, Lokale: Banach-Tarski im Licht moderner Mathematik!

Lässt sich eine Kugel verdoppeln, indem man sie zerteilt und ihre Einzelteile neu anordnet? Im wirklichen Leben funktioniert das nicht, doch in der Mathematik scheint es möglich zu sein – zumindest, wenn es nach einem Satz der Mathematiker Stefan Banach und Alfred Tarski geht. Chiara Cimino und Christian Krause gingen dieser paradoxen Aussage auf den Grund. Dabei stießen sie auf eine bislang unveröffentlichte Arbeit aus Frankreich. Sie beschreibt einen Weg, wie sich das Paradoxon auflösen lässt. Um die Beweisführung zu überprüfen, nutzten die beiden eine Software namens Lean, mit der sich mathematische Beweise formal und fehlerfrei überprüfen lassen. Damit gelang es, manche Lücke in der Theorie der französischen Mathematiker zu schließen und der Auflösung des Kugelparadoxons ein gutes Stück näherzukommen.