ИИ-агенты впервые компьютерно проверили самое длинное доказательство в истории математики
ИИ-агенты впервые компьютерно проверили самое длинное доказательство в истории математики Классификация конечных простых групп насчитывает около 15 000 страниц и была написана примерно 100 математиками на протяжении десятилетий. За 24 дня команда Axiom направила рои ИИ-агентов на эту задачу и перевела всё доказательство в Lean — язык, в котором компьютер проверяет каждый логический шаг. Результат — около 43,1 миллиона строк кода. Агенты распределяли задачи, передавали недостающие фрагменты другим агентам и объединяли свою работу в едином репозитории. Они также обнаружили реальные проблемы в опубликованном доказательстве. Большинство из них были опечатками и ошибками в таблицах, но, по словам Axiom, 34 отклонения пришлось исправить. 🖥Мы в Телеграм Новости IT Всемм 💻Мы в Max Новости IT Всемм