Formalisierung des Fermatschen Letzten Satzes in Lean: Ein Open-Source-Projekt

Ein ehrgeiziges Open-Source-Projekt zielt darauf ab, den Fermatschen Letzten Satz formal mit dem Lean-Theorembeweiser zu beweisen. Geleitet von Kevin Buzzard und finanziert von der EPSRC, gehostet am Imperial College London, verwendet das Projekt eine moderne Variante des ursprünglichen Wiles/Taylor-Wiles-Beweises, der in Zusammenarbeit mit Richard Taylor geplant wurde. Die Projektwebsite enthält Details zum Fermatschen Letzten Satz, zum Lean-Beweiser, zu den Projektzielen und zu den Beitragsrichtlinien.