OpenAI выложила сотни решений сложных математических задач — и математики встретили это не фанфарами, а вопросом: кто вообще за эти доказательства отвечает?
Повод жирный: в релизе фигурируют 719 рукописей. Но прозрачность там не такая широкая, как хотелось бы людям, которые потом должны читать, проверять и объяснять эти результаты. Полные цепочки рассуждений модели есть только у 10 работ. А с формализацией тоже не всё гладко: в материале отдельно сказано про 42% доказательств и процесс перевода в Lean — язык, где математическое доказательство можно проверить как код.
Lean тут важен, но это не печать «всё, истина». Если обычный текст доказательства и Lean-код разъехались по смыслу, компилятор не спасает. Он проверяет код, а не то, что этот код честно передал исходную идею. Именно такой риск показала отдельная работа математиков из Кембриджа и King’s College London: в решении, связанном с задачей из области уравнений Навье — Стокса, нашли как минимум два расхождения между текстом и Lean-версией.
Есть ещё неприятный контекст. AGMAI, группа математиков при Institute for Advanced Study, незадолго до этого выпустила рекомендации для AI-лабораторий. Первый пункт звучал совсем не дипломатично: не тестировать продвинутые открытые математические задачи на закрытых проприетарных моделях. OpenAI как раз пишет, что оценивает свои закрытые модели на открытых исследовательских задачах. Ну то есть мимо кассы, аккуратно говоря.
Смысл не в том, что все решения OpenAI неправильные. Этого из источника не следует. Смысл в другом: математика — не табличка лидеров, где модель выбила красивый результат и все пошли домой. Новое доказательство должно быть понятно людям, выдерживать вопросы, семинары, рецензирование и нормальную научную драку.
Пока OpenAI принесла не готовую полку с новыми теоремами, а большую коробку деталей. Где-то там может быть ценное железо. Но собирать, сверять и объяснять его всё равно придётся людям.