У математиков случилось то, что скоро случится почти в любой профессии. Матокалипсис!

У математиков случилось то, что скоро случится почти в любой профессии. Матокалипсис!

За драмой можно наблюдать прям сейчас, там очень весело и интересно. Началось с того, что в августе OpenAI собрала 40 математиков на встречу с интригующим названием «Конец математики». Если коротко — в одном из вариантов человеческая помощь моделям нафиг уже не нужна, спасибо, мясные, отойдите, пожалуйста.

Ещё математики там попросили публиковать всё статьями, но OpenAI всё выбросила постами, типа, сношайтесь там сами. Пока они сношались, то заметили, что идеи машинных доказательств бывают подозрительно похожи на их неопубликованные наработки, которые они обсуждали с OpenAI.

8 сентября OpenAI сказала, что её закрытая модель решила проблему Навье-Стокса. Это, если что, штука, которую люди решить не могли. За пару часов до этого ещё один товарищ со спецом из Антропика шли тем же путём и были близко, но OpenAI узнала про это и рванула наперегонки. Ещё ему предложили сделку (с его слов): писать статью вместе с OpenAI, но без коллеги Альпёге, потому что тот работает у конкурента. OpenAI сказали, что это всё ужасная ошибка, и они взяли 10 тысяч агентов на 88 часов.

Дальше офигенная цепочка событий: — 25 топовых математиков подписали декларацию: цели ИИ-компаний и математики резко расходятся, результаты объявляются в спешке, без нормального изложения и ссылок на предшественников, что пахнет плагиатом. — OpenAI сняла спонсорство с одного из мероприятий, где было дофига участников декларации. — OpenAI завела консультативную группу математиков. Группа сразу попросила не гонять сложные задачи на закрытых моделях. — 6 октября выложила 722 рукописи закрытой модели и сказала, что сношайтесь всё же, потому что тут многие результаты не понимают даже встроенные в компанию математики. Вроде, за день до этого учёные в панике публиковали свои неоконченные работы, чтобы их не обогнали. — Объяснили такой скотский подход (с точки зрения математиков) тем, что OpenAI и Anthropic готовятся к IPO. — Крупная ассоциация математиков предложила объявить бойкот OpenAI. В них в ответ покидали деньгами.

Дальше жопа сгорела у всего сообщества, потому что несмотря на скотский подход, доказательства-то реальные, и наука двигается. Можно истерить, но наука двигается. Но там море проблем: — У многих опустились руки — нет смысла думать над такими задачами, потому что робот всё решит. — Есть такой Йорг Нойнхойзерер, который всю жизнь решал три задачи и не решил, а ChatGPT походя их закрыл. Ну сорян, чо. — Профессор Лосано-Робледо опубликовал письмо студента, который мечтал об академической карьере, а теперь не понимает, останется ли в математике место для кого-то, кроме гениев. Таких писем вроде бы много. Процесс тоже поменялся: аспирантам теперь спускают машинные доказательства на переписывание.

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

Тут работа про то, как проверять доказательства, потому что моделям верить на слово нельзя. Предлагают точно так же, как в разработке — писать скрипт и исполнять. Конкретно выгружать доказательство на языке Lean, который исполняется компилятором. Собственно, основная проблема теперь — оно стало всё проверяемо, но НИХРЕНА НЕПОНЯТНО, как работает.

За последнюю неделю выяснилось, что Lean-формализация Навье-Стокса не совпадает с доказательством в самой статье, так что третья черепаха врёт. Ну и предложили математику 2.0 — решать не надо, надо объяснять.

Добро пожаловать в матокалипсис!

— Вступайте в ряды Фурье! | Лучшие посты 350 лет без рекламаций! Без документации! Без инструкций! Без поддержки! Теорема Ферма!