Sechs-Sphäre: Lösung des Hopf-Problems in Lean formalisiert

Formalization of the Solution to the Hopf Problem

Ein neues Repository formalisiert in Lean die Lösung des Hopf-Problems: Die sechsdimensionale Sphäre besitzt eine komplexe Mannigfaltigkeitsstruktur, die mit ihrer Standardtopologie kompatibel ist. Die Arbeit basiert auf einem Beweis von Levent Alpöge und wurde in den Formalisierungswettbewerb von DeepMind integriert. Das Projekt enthält eine Comparator-Konfiguration und kann direkt im Browser überprüft werden.