Компания Axiom Math, разрабатывающая инструменты для формальной верификации математических моделей, объявила о сотрудничестве с профессором Гарвардского университета Скоттом Коминерсом (Scott Kominers) для кодификации теоремы согласия Роберта Ауманна в системе компьютерной проверки доказательств.
Axiom Math и экономист Скотт Коминерс завершили формальное доказательство теоремы согласия Ауманна — фундаментального результата в теории игр, описывающего условия, при которых рациональные агенты с общей априорной информацией не могут «согласиться не согласиться». Работа выполнена на базе языка программирования Lean, используемого для математической верификации.
Теорема, сформулированная израильским экономистом Робертом Ауманном в 1976 году, лежит в основе современной теории рационального принятия решений. Её формализация позволяет применять результаты в экономических моделях с гарантированной корректностью, исключая ошибки, связанные с неявными допущениями или неполными доказательствами. Как отметил Коминерс, «верифицированное доказательство устраняет неопределённость в интерпретации условий теоремы, что критически важно для прикладных исследований».
Проект реализован в рамках инициативы Axiom Math по созданию библиотеки формализованных экономических и математических теорем. Компания позиционирует свои разработки как инструмент для академических исследований и финансовых институтов, где требуется высокая степень доверия к моделям. Ранее Axiom Math уже представила формальные доказательства теоремы о невозможности Эрроу и модели общего равновесия Эрроу—Дебре.
Результаты работы доступны в репозитории Axiom Math на платформе GitHub. По словам представителей стартапа, формализация теоремы Ауманна — первый шаг к созданию верифицируемой базы для анализа динамических игр и механизмов принятия решений в условиях неопределённости.
Источники: X-пост Скотта Коминерса, 1 июня 2026; блог Axiom Math.