La classificazione dei gruppi semplici finiti diventa, secondo Axiom Math, una dimostrazione interamente verificabile in Lean. Ma dietro i ventiquattro giorni annunciati c’è una storia di decenni, di altre formalizzazioni già in corso e perfino di un problema inatteso in un teorema della classificazione. Marco Trombetti torna sul teorema enorme. Qualche tempo fa, proprio sulle […]L'articolo Je n’ai pas le temps, ma l’IA sì: il teorema enorme, 43 milioni di righe e qualche sorpresa proviene da Maddmaths!.