OpenAI вывалили на GitHub 722 математические статьи от своей внутренней модели. Одним релизом :)

Да, тоже было интересно разобраться, что там вышло. Математикам тоже приготовиться на выход?

Короче, в сентябре они заявили, что решили одну из задач тысячелетия (за каждую дают $1M) – 88 часов, тысячи агентов параллельно. После этого 25 лауреатов Филдсовской премии (математический «Нобель», там и Теренс Тао) подписали открытое письмо: вы решаете задачи как бенчмарк, а математике нужно понимание. OpenAI сходили посоветоваться с математиками из Принстона и... выложили ещё 722 статьи :)

Модели дали ~4000 открытых задач, на которых люди застряли. Из этого получилось 722 статьи с решениями.
– В среднем 3 часа думанья уровня ChatGPT Pro на результат. Не суперкластер, а примерно то, что вы можете сделать сами за вечер, только модель внутренняя
– 162 доказательства проверены в Lean. Это такой язык программирования для математики: доказательство пишется как код, и компьютер его проверяет как компилятор. Скомпилировалось – значит без ошибок. Остальные 560 никто толком не проверял, в README так и написано: «могут быть ошибки»

Что из этого понятно не только математикам:
– Гипотеза уникальных игр. Она про то, какие задачи оптимизации в принципе нельзя решить хорошо даже приблизительно. Из доказательства следует, что для кучи практических задач (разбить сеть на части, раскидать ресурсы, кластеризовать) нынешние алгоритмы уже лучшие из возможных, и искать лучше бессмысленно. Проверено в Lean
– «Почти гипотеза Римана». Сама гипотеза Римана – главная нерешённая задача математики, про то, насколько равномерно разбросаны простые числа. Её ослабленную версию не могли доказать с XIX века. Модель доказала. Тоже в Lean
– Нельзя написать программу, которая для любого уравнения скажет, есть ли у него решение в дробях. Вопрос висел десятилетиями. Без Lean
– Кусок ещё одной задачи тысячелетия (гипотеза Ходжа). Объяснить на пальцах её не может никто, так что поверим на слово :)

Но!
– Самые громкие результаты получены не той стандартной процедурой на 3 часа, а отдельно, и один текст правили люди
– Lean проверяет, что код соответствует ТЗ. А правильно ли написано само ТЗ, то есть то ли вообще доказали, – всё равно смотреть людям
– Авторов нет, всё подписано «OpenAI». Модель не выпущена, обещают «ответственный релиз»

Прикол, что письмо было ровно про то, что математикам не нужны сотни решённых задач без понимания. В ответ им дали 722 решённые задачи, но с компиляцией и пересказами того, как модель думала :)

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

https://openai.com/index/sharing-ai-progress-in-mathematics/