Lean überprüft den Beweis des größten Satzes der Gruppentheorie

Classification of Finite Simple Groups Formalized in Lean

Die Klassifikation der endlichen einfachen Gruppen gilt als eines der größten Gemeinschaftswerke der Mathematik: Rund hundert Mathematiker schrieben über Jahrzehnte Tausende von Seiten. Nun liegt der Beweis der ersten Generation vollständig in Lean formalisiert vor – 43,1 Millionen Zeilen, jeder logische Schritt vom Kernel geprüft. Dabei stießen die Beteiligten auf ein Problem in einem veröffentlichten Argument für das Unbalanced Group Theorem und fanden einen alternativen Weg.