Anthropic объявила о первой полной сквозной формализации Великой теоремы Ферма: система Claude записала доказательство на языке Lean, а компьютер проверил всю логическую цепочку от исходных предпосылок до конечного утверждения. Работа заняла 11 дней, потребовала около шести миллиардов выходных токенов и породила 13 миллионов строк кода. Звучит так, будто искусственный интеллект за полторы недели решил задачу, над которой математики бились три с половиной века. Но это не совсем так. Claude не нашёл...