Lean-Beweisprüfer: Fermats großer Satz in elf Tagen durch KI verifiziert

Eine Million Pfund, fünf Jahre Zeit: So wollte der Mathematiker Kevin Buzzard den Satz von Fermat formalisieren. Dann erledigte ein KI-Modell diese Aufgabe in nur elf Tagen.