III. Понятие доказательства: программы и теоремы
ИИ перевел доказательство Великой теоремы Ферма в код всего за 11 дней
Модель Claude формализовала доказательство Великой теоремы Ферма «в основном автономно» всего за 11 дней, сообщила компания-разработчик Anthropic. Полученный результат представляет собой 13 миллионов строк кода на Lean — специальном математическом инструментарии. Великая теорема Ферма веками не давала покоя математикам, пока в 1995 году ее не доказал Эндрю Уайлс. Она гласит, что не существует таких целых чисел a, b и c, которые удовлетворяли бы уравнению aⁿ + bⁿ = cⁿ, где n — целое число больше 2...