Алгоритмы Anthropic формализовали доказательство теоремы Ферма за 11 суток

Нейросетевая модель Claude от компании Anthropic успешно перевела сложнейшее математическое доказательство в компьютерный код менее чем за две недели.

Искусственный интеллект справился с задачей, на которую ученые планировали потратить годы, пишет «New Scientist».

Группа автономных ИИ-агентов подтвердила правильность решения, предложенного Эндрю Уайлсом в 1995 году.

«На этом пути мы видим автоформализацию алгебры, гармонического анализа, геометрии и теории чисел, и мы узнаем, что артефакты автоформализации ИИ теперь достаточно надежны, чтобы на них можно было опираться; доказательство многослойно», – заявил математик Кевин Баззард.

Ученый добавил, что успех проекта означает гигантский шаг к автоматической формализации современной математической литературы. Модель непрерывно работала 11 дней, разделив теорему на небольшие фрагменты для разных агентов.

Итоговый код на языке Lean содержит 13 млн строк и охватывает почти 29,5 тыс. промежуточных теорем. Это делает его самым масштабным доказательством в истории базы Mathlib.

Как писала газета ВЗГЛЯД, британские исследователи запустили проект по оцифровке доказательства великой теоремы Ферма с помощью искусственного интеллекта.

В прошлом месяце нейросеть компании Anthropic самостоятельно уволила реального продавца из магазина в Сан-Франциско за регулярные прогулы.

Ранее передовая модель этого американского разработчика за несколько часов взломала секретные базы Агентства национальной безопасности США.