Claude sformalizował dowód twierdzenia Fermata w 11 dni

Model AI Claude od Anthropic stworzył kompletną, weryfikowalną komputerowo formalizację dowodu wielkiego twierdzenia Fermata — zadania, z którym przez lata mierzyli się najwybitniejsi matematycy. Praca zajęła modelowi zaledwie 11 dni i zaowocowała około 13 milionami linii kodu w języku Lean. To przełomowy przykład zastosowania sztucznej inteligencji w matematyce formalnej.