ИИ формализовал доказательство теоремы Ферма за 11 дней

Экспериментальная версия Claude перевела доказательство последней теоремы Ферма в 13 миллионов строк компьютерно проверяемого кода. Впервые знаменитый результат, доказанный Эндрю Уайлсом, получил полную формальную запись, которую может последовательно проверить программа.

ИИ не открывал теорему заново, а преобразовал существующее доказательство в строгую машинную форму. Такая технология может ускорить проверку сложных математических работ, хотя полученный массив кода пока нельзя сразу добавить в общую библиотеку Mathlib.