Первого августа OpenAI выложила десять результатов по математике, которые получила внутренняя версия их следующей модели — Astra. Наружу её пока не давали. Каждая задача стояла минимум десять лет, часть — гораздо дольше.
Там несофические группы (Громов ввёл софичность в 1999-м, и с тех пор никто не мог предъявить группу, которая ей не удовлетворяет), опровержение гипотезы жёсткости Конна про алгебры фон Неймана, гипотеза Эрхарта об объёме, три задачи Эрдёша и первое с 1978 года улучшение общих верхних оценок плотности упаковки шаров в больших размерностях.
Оценивать «важность» этого списка я не возьмусь — не моя специальность, и вообще с важностью в математике всегда было сложно. Задачу решают сейчас, а где это применить, выясняется лет через сорок, и обычно совсем не там, где ждали. Но одну вещь заметить могу: шкала растёт, причём быстро. Два года назад спорили, сможет ли ЛЛМ написать межнар хоть как-нибудь. Сейчас новость «большинство моделей пишут на 42 из 42» проходит мимо, потому что это уже даже не круто. Год назад тут была мелочь, и все говорили, что серьёзного никогда не будет. В этом месяце это точно уже не мелочь. А когда начнут щёлкать задачи тысячелетия, мы вполне можем оказаться не готовы к тому, что с этим делать.
Теперь про то, ради чего я вообще пишу.
Все десять доказательств выложены с сертификатами на Lean 4 — гитхаб, Apache-2.0, клонируй и собирай. Сам я проверять не буду: наверняка кто-то из математиков уже собрал, и глупо было бы врать именно в этом месте — это ловится за полчаса.
Раньше главный вопрос ко всем таким новостям был «ну и кто это будет читать». Я писал про 728-ю задачу Эрдёша, и там в комментариях спрашивали ровно то, что надо: а как вы проверите, что ИИ правильно перевёл формулировку в Lean? Вопрос никуда не делся. Lean гарантирует, что из формальных посылок формально следует формальное заключение. Что эти посылки — та самая гипотеза Конна, а не соседняя, по-прежнему смотрит человек глазами. Но это другой объём работы, чем читать 249 страниц с нуля.
И вот тут интересно накладывается июньская Лейденская декларация. (Коротко: математики обеспокоены, что результаты льются не туда и предлагают всем все таки использовать научные журналы). Её поддержал IMU, за сутки подписала тысяча человек, и один из пунктов — не выносить результаты в прессу в обход рецензирования. Через два месяца прилетает блогпост с десятью теоремами.
С одной стороны, декларация права. В момент, когда любой может выкатить громкий заголовок, фильтр нужен — иначе мы утонем.
С другой — институт, который она защищает, уже давно не в лучшей форме, и не из-за ИИ. Платят за публикацию авторы, а не журнал за контент. В узких областях тебя рецензируют полтора человека из соседней лаборатории, с которой ты завтра будешь делить грант. Лобби производителей. Невоспроизводимые результаты, которые годами никто не перепроверяет, потому что за перепроверку не платят и статью из неё не сделаешь. Так что гитхаб с твиттером вместо журнала — это не только маркетинг. Это ещё и «нам проще не связываться».
И дальше выходит почти обидно. Рецензирование — это институт доверия: ты веришь, что уважаемый человек прочитал и не соврал. Lean-сертификат доверия не требует вообще — ни к OpenAI, ни к рецензенту, ни к автору. Собирается — значит выведено. Декларация защищает процедуру, Lean защищает истину, и в этот раз они оказались по разные стороны.
Хотя от доверия мы, конечно, не ушли. Мы его сжали до одной строчки — той самой, где формулировка на Lean должна совпасть с гипотезой, о которой все думают.
Ну и то, что проверить нельзя вообще никак: сама Astra закрыта. «Доказано ли» — проверяемо. «Правда ли так быстро и за такие деньги» — только на слово.
