Claude за 11 дней доказал великую теорему Ферма — впервые в полностью проверяемом компьютером виде
Formalizing Fermat's Last Theorem
Исследователи Anthropic сообщают, что их ИИ-модель Claude впервые в истории формализовала доказательство великой теоремы Ферма — одной из самых сложных математических задач. Работая почти автономно в течение 11 дней, Claude написал 13 миллионов строк кода на языке Lean и доказал 29 500 промежуточных теорем. Формализация, проверенная компьютером, устраняет любые сомнения в корректности доказательства, что может стать шагом к автоматической проверке всей математической литературы.
Это необычайное достижение автоформализации, которое, по словам исследователей Anthropic, заняло всего 11 дней, доказывает великую теорему Ферма без каких-либо допущений, кроме аксиом математики.