11 дней вместо лет: Claude переписал теорему Ферма на язык машины
11 дней вместо лет: Claude переписал теорему Ферма на язык машины Anthropic опубликовала первое сквозное компьютерно проверяемое доказательство Великой теоремы Ферма. Агенты Claude за 11 дней записали его в Lean — языке, где каждое утверждение проверяет компьютер. Это не новое решение: теорему доказали Уайлс и Тейлор в 1995 году. Формализация изложения Дармона–Даймонда–Тейлора дала 13 млн строк и около 29 500 промежуточных теорем. Кевин Баззард из Imperial College, который вёл многолетний проект той же работы, назвал итог выдающимся: это не новая математика, а проверка известного пути. Машина не открыла теорему. Она сняла нужду верить доказательству «на слово»... Источники: https://www.anthropic.com/research/formalizing-fermats-last-theorem https://www.newscientist.com/article/2587839-fermats-last-theorem-formalised-by-ai-agents-in-just-11-days/ #AI #Anthropic #Claude #Lean #FLT #MathAI
Канал в каталоге Максиметера
547 подписчиков · IT и технологии