ИИ помог создать первое полное компьютерно-проверяемое доказательство Огромной теоремы

Axiom Mat успешно завершила компьютерную формализацию Огромной теоремы

Компания Аксиом Мат достигла исторического рубежа, завершив масштабную задачу по компьютерной формализации Огромной теоремы. Речь идет о классификации конечных простых групп — одном из самых значимых достижений математики XX века, над доказательством которого ученые трудились более пятидесяти лет. Для обеспечения безупречной точности проверки первого поколения доказательства исследователи применили возможности языка программирования Лин.

Ключевым фактором успеха стал беспрецедентный масштаб применения технологий искусственного интеллекта. Всего за двадцать четыре дня десятки специализированных ИИ-агентов смогли сгенерировать более сорока трех миллионов строк кода. Этот процесс позволил автоматизировать проверку сложнейших математических цепочек, обеспечивая глубину анализа, которая ранее была практически недоступна человеческому вниманию в таких масштабах.

В ходе автоматизированной проверки система обнаружила тридцать четыре существенных расхождения в ранее опубликованных материалах. Более того, интеллектуальные агенты даже нашли контрпримеры к утверждениям, которые долгое время считались истинными. Это вынудило команду исследователей пересматривать логические цепочки и разрабатывать принципиально новые математические аргументы для устранения выявленных ошибок.

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