ИИ впервые проверил сложнейшее математическое доказательство — но не всё так гладко

Команда стартапа Axiom Math отчиталась о первом успешном применении ИИ-системы AxiomProver для формальной проверки доказательства так называемой «теоремы 246» — одной из сложнейших современных теорем о простых числах. Формальная верификация означает, что компьютер проанализировал машиночитаемую версию доказательства и подтвердил её корректность.

Впрочем, разработчики признают, что метод не даёт 100-процентной гарантии. В ходе демонстрации была выявлена принципиальная проблема: если в процессе проверки допущена ошибка в самом подходе, ИИ может ложно «подтвердить» неверное доказательство. Тем не менее, это наиболее близкий к достоверности способ автоматической верификации на сегодня.

Помимо ценности для теории чисел, пример демонстрирует потенциал технологии для более прикладных задач. В будущем аналогичные системы смогут проверять корректность ИИ-сгенерированного кода, который всё чаще становится основой глобального ПО.

Хотя до полной автоматизации математической верификации ещё далеко, работа Axiom Math — важный шаг к тому, чтобы ИИ не только создавал, но и надёжно проверял результаты своей деятельности.