Множество доказательств, выданных ИИ, — не всегда однозначное благо... Математическое сообщество уже не успевает их все читать.
Однако есть и хорошие новости —
Перед лицом этого кризиса два обладателя Филдсовской премии, Терри Тао и Ван Хун, дали практически идентичную оценку:
Переваривание.
Недавно факультет математики Пекинского университета опубликовал большое интервью с Ван Хун, где она дала весьма взвешенный совет:
Математическое сообщество не может игнорировать контрпримеры или доказательства, сгенерированные ИИ; нам нужно учиться их использовать, а также понимать и переваривать.
Терри Тао же потратил несколько дней, чтобы полностью переварить доказательство, выполненное при участии ИИ.
Это доказательство решает гипотезу Сендова, остававшуюся открытой 67 лет.
Звучит несколько парадоксально. Раз ИИ создан, чтобы помогать математикам решать задачи, и ответ уже получен, зачем же его снова «переваривать»?
«Провозвестник» Терри Тао дает такой ответ:
Корректное доказательство — это лишь первый этап математического результата; его ещё должны понять и усвоить профессиональные математики, чтобы он стал полностью пригодным к использованию.
Проводя аналогию, традиционный автор подобен ответственному родителю, который полностью сопровождает доказательство от рождения до публикации, тогда как в будущем при работе с ИИ эти отношения могут стать больше похожими на «усыновление»:
Одна группа людей с помощью ИИ продвигает доказательство до стадии генерации или проверки, а затем официально передает эстафету другой группе для профессиональной интерпретации, систематизации и публикации.
Математикам по-прежнему есть, где приложить силы.
Переваривание — следующий шаг в решении векового кризиса математики
По сути, это ответ Терри Тао на вопрос, который он сам задал месяц назад на своем выступлении на Международном конгрессе математиков (ICM):
Если ответы могут быть массово произведены ИИ, то к чему тогда стремиться в математических исследованиях?
Новая модель OpenAI Astra решила 10 сложных задач из области математики и теоретической информатики, охватывающих многомерную геометрию, теорию кодирования, теорию групп и другие области.
Нейрохирург без формального высшего математического образования, позволив ChatGPT 5.6 автономно работать около 16 часов, получил ключевое доказательство гипотезы Крузе в численной линейной алгебре.
......
Кажется, ИИ прорубил черный ход в высокую стену математики.
Если даже непрофессионалы могут с его помощью прорываться к передовым проблемам, не станет ли математика «следующим строительным делом»? (шутка)
Вовсе нет! На самом деле, полноценный математический результат никогда не ограничивается только этапом «получения доказательства».
Терри Тао разбивает его на пять этапов:
Сначала генерируется аргументация, затем проверяется её корректность; далее нужно объяснить идеи коллегам, чтобы результат прошел публикацию и проверку сообществом; наконец, результат нужно реорганизовать, найти его связь с существующими теориями и превратить в стандартное знание, доступное для будущего использования.
ИИ сейчас лучше всего ускоряет первые два шага. Чем дальше, тем больше требуется суждения математика о том, где заключается суть и что означают результаты.
А гипотеза Сендова, с которой только что работал Терри Тао, стала почти идеальной практической демонстрацией этого процесса.
Эта гипотеза изучает расстояние между нулями полинома и его критическими точками. Предыдущие результаты уже решили случаи для низких степеней и достаточно больших степеней, средний диапазон долгое время оставался открытым.
Несколько дней назад математик-любитель Лех Мазур с использованием ИИ заполнил этот пробел и представил формализованное доказательство, проверенное в Lean.
Казалось бы, на этом история должна была бы завершиться. Однако Терри Тао заметил, что это исходное доказательство ещё не было оформлено в математический текст, пригодный для чтения и публикации людьми, то есть математический результат ещё нельзя было использовать.
Поэтому он потратил несколько дней на полное переваривание результата, используя помощь как ChatGPT, так и ручных вычислений:
проследил источники литературы → выделил действительно работающие тождества → убрал лишние обходные пути → переписал аргументы, найденные машиной, в версию с видимой основной линией рассуждений.
Это прочтение, в свою очередь, выявило кое-что новое.
Систематизированная аргументация не только решает гипотезу Сендова, но и покрывает более сильную гипотезу Фелпса–Родригеса. Необходимые ключевые инструменты также оказались более элементарными, чем это представлялось в исходной формализации: код Lean сократился примерно с 90 000 строк до 15 000.
Другими словами, переваривание — это не только повторная проверка доказательства ИИ, но и эффективный путь к расширению математических результатов.
Что ещё важнее, Терри Тао с помощью идеи переваривания хочет пересмотреть старую систему правил в математическом сообществе, основанную на принципе «кто первый объявил — тому и приоритет».
Принадлежность математического результата изначально определялась датой публикации в журнале, позже — временной меткой в arXiv.
Сегодня доказательства от ИИ появляются слишком быстро, даже arXiv кажется кому-то медленным, и некоторые результаты выкладываются в социальные сети сразу после генерации. В погоне за первенством этапы проверки и интерпретации полностью пропускаются, что в конечном итоге создает для математического сообщества дополнительную нагрузку.
Поэтому в своем выступлении на ICM Терри Тао призвал математическое сообщество прекратить безоглядно возвеличивать «того, кто первым дал доказательство», и повысить статус работы по «перевариванию и систематизации доказательств».
Объяснение доказательств, рецензирование, приведение результатов в соответствие с классической теорией — вся эта работа также должна цениться, нельзя считать заслугой только создание новых теорем.
Если авторы статьи сами не могут сделать доклад на уровне специалиста и внятно объяснить результат, то как бы правильно ИИ его ни проверил, такая работа не должна публиковаться.
Доказательство, которое люди не могут понять, нельзя считать завершенным результатом.
Поэтому Терри Тао призывает научное сообщество спокойно собраться и провести глубокое обсуждение как пределов возможностей ИИ и ценностей математики, так и подчеркнуть те аспекты математической работы, которые не могут быть заменены машиной.
И ещё кое-что
Параллельно с этим Терри Тао также создал и открыто представил реестр для результатов, проверенных в Lean, — Palomar.
Palomar будет четко регистрировать формулировку задачи, код доказательства, способ и версию участия ИИ, а затем, после независимой проверки ядром, собирать в одном месте доказательства от ИИ, разбросанные по GitHub, соцсетям и новостям.
Он будет служить промежуточной станцией для переваривания между проверкой и публикацией, позволяя последующим исследователям знать, что уже сделано ИИ и коллегами, и какая работа ещё осталась.
Команды, интересующиеся одной и той же проблемой, могут сотрудничать в исследованиях через Palomar.
Важно отметить, что Palomar не отвечает за оценку важности того или иного результата и не заменяет рецензирование коллегами.
Права на конкретный результат в будущем будут определяться последовательностью четырех временных точек:
Результат генерации, фиксирующий, как было получено доказательство, например, история чата с ИИ;
Результат проверки, подтверждающий логическую корректность, например, код Lean;
Результат интерпретации, объясняющий идеи, например, публичное выступление;
Опубликованный результат, официально представляющий результат, например, статья.
Иными словами, приоритет получает тот, кто первым представит полный набор завершенных результатов.
В настоящее время систематизированная Терри Тао гипотеза Сендова стала одним из первых документов в Palomar.
Ссылки:
[1]https://arxiv.org/abs/2608.16753
[2]https://mathstodon.xyz/@tao/117123957813926355
[3]https://www.youtube.com/watch?v=M0--ZH1lOzg
[4]https://mp.weixin.qq.com/s/w-UfVMmwTZqXjNsC81CzYw
Эта статья взята из официального аккаунта WeChat «Квантовый бит» (量子位), автор: «Следим за передовыми технологиями».
