Оглавление

Компания OpenAI представила внушительный массив из 372 математических результатов, сгенерированных внутренней ИИ-моделью, фактически предложив академическому сообществу адаптироваться к новым скоростям производства знаний. Как сообщает издание The Decoder, опубликованные данные включают в себя продвижение в решении открытых проблем, улучшения алгоритмов и даже шаги в сторону доказательства гипотезы Римана.

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

Формальная верификация как новый стандарт рецензирования

Чтобы справиться с потенциальным скепсисом и объемом данных, OpenAI снабдила многие доказательства формализацией на языке Lean. Это специализированный язык программирования, позволяющий машине автоматически проверять логическую корректность математических выкладок. Использование Lean становится практической необходимостью: человеческий ресурс для ручной проверки сотен сгенерированных страниц просто не масштабируется под темпы работы нейросетей.

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

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

Реакция математического сообщества и этические границы

Хотя OpenAI консультировалась с консультативной группой при Институте перспективных исследований, в которую входит лауреат премии Филдса Тимоти Гауэрс, компания установила жесткие рамки: математики могут советовать, как представлять результаты, но не влиять на темпы их производства. Это создает определенное напряжение, ведь многие ученые опасаются, что ИИ может сделать их область менее «человечной».

Критики, включая 25 обладателей Филдсовской премии, в открытом письме предупредили, что погоня за количеством доказанных теорем подменяет истинную цель математики — понимание сути вещей. Они полагают, что избыток «машинных» знаний может разрушить образовательную среду, где интуиция и озарение ценятся выше, чем простой перебор вариантов.

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