Команда Fundamental AI Research (FAIR) компании Meta при поддержке Superintelligence Labs применила ИИ-модели для решения шести открытых математических задач. Результаты работы представлены в серии из шести научных публикаций, где ИИ выступает как инструмент для совместной работы с математиками.
Одним из значимых результатов стало опровержение гипотезы Гарсия-Мартинеса и Перес-Родригеса об алгебрах эволюции, представленное 2 октября 2026 года. Ранее, 23 сентября 2026 года, Meta опубликовала препринт «Learning to Discover Interesting Mathematics», посвященный генерации теорем с помощью языковых моделей.
В мае 2026 года компания запустила систему AutoformBot, которая перевела 26 учебников по математике на язык ассистента доказательств Lean 4. В результате была создана библиотека, включающая более 45 000 деклараций и сотни тысяч строк верифицированного кода для автоматизации формализации доказательств.
В 2026 году область математики с поддержкой ИИ активно развивается: свои исследования публикуют OpenAI и Google DeepMind. В большинстве работ, включая проекты Meta, используется формальная верификация через систему Lean, позволяющая подтверждать корректность выводов, полученных с помощью машинного обучения.
