ИИ и перспективы математики и математического образования

[Ghost_of_past]

(Оффтоп)

mihaild в сообщении #1729660 писал(а):

Это политика всего бигтеха (как минимум). Любое не прошедшее 50 этапов согласования высказывание должно помечаться как личное мнение сотрудника*.
[*] это моё личное мнение, которое может отличаться от официальной позиции компании

Не только бигтеха и даже не только коммерческого сектора. У меня и в университете нельзя давать журналистам/блогерам ответы на вопросы с пометкой, что являешься сотрудником университета, без согласования с пресс-службой университета.

[MoonWatcher]

Цитата:

Долго ждать не пришлось: OpenAI выложили результаты, полученные моделью Astra (официально подтвердили название). Блогпост называется «Десять достижений в математике и теоретической информатике»

Мне трудно осознать всю сложность этих задач. Я не то что математик, у меня диплома-то даже нет 😀 и я не вижу разницы, скажем, между 3-м и 10-м результатами.

Поэтому я попросил GPT-5.6 Sol Pro и Fable 5 Max (чтоб не было позитивного биаса на OpenAI) классифицировать их, используя систему критериев задач в бенчмарке OpenMath от EpochAI:

🟢 «Значимый результат» (Solid Result): Сильный исследователь в данной области был бы рад, если бы его среднестатистическая работа решала задачи такого уровня. Тем не менее, за пределами узкой специализации эта проблема вряд ли вызвала бы большой резонанс.
🟡 «Крупное достижение» (Major Advance): Среднестатистический специалист, работающий в широкой области математики (в масштабах теории чисел или теории графов), обратил бы на это внимание и, скорее всего, нашел бы время, чтобы вникнуть хотя бы в общую суть решения.
🔴 «Прорыв» (Breakthrough): Среднестатистический математик захотел бы узнать об этом результате, даже если он выходит за рамки его специализации. Такая работа стала бы кандидатом на звание одного из лучших результатов года во всей математике.

Обе модели — и Fable, и Sol — сошлись во мнении, что результат №3 — это «Прорыв» (что объясняет, почему сотрудник OpenAI из всех выделяет именно его в своём твите).

Они также согласны, что как минимум 7 решений из 10 относятся к категории «Крупное достижение».

Что еще интересно, в официальных критериях EpochAI сказано следующее:
«Когда для задачи подходили сразу несколько уровней оценки, мы склонялись к более консервативному варианту. Было бы неприятно понижать статус задачи уже после того, как она решена, в то время как мы всегда можем подчеркнуть любые неожиданно интересные элементы в самом решении».

И Fable 5 считает, что как минимум три результата находятся на грани «Прорыва» (№1, №4 и №9).

Все решения проверены в Lean — языке программирования для доказательства теорем. Если решение компилируется без ошибок, то оно либо правильное, либо есть баг в самом ядре (такое тоже бывало, но маловероятно, что все 10 результатов — результат бага проверки).

Суммарно на решение 10 задач потратили ~$2000 по API-ценам Sol (то есть скорее всего будет в 2 раза больше)

[worm2]

MoonWatcher в сообщении #1729683 писал(а):

Суммарно на решение 10 задач потратили ~$2000 по API-ценам Sol (то есть скорее всего будет в 2 раза больше)

А они по-честному считали?
А то может случиться так, что я вчера поднял на бирже 10 тыс. долларов. Но не упоминаю о том, сколько я вообще играл (хотя бы на этой бирже и хотя бы в этом году), и каков общий баланс (за это время в этом месте хотя бы).

[MoonWatcher]

worm2
А как можно посчитать нечестно? Учет затраченных на решение задачи токенов ведется - остается только умножить их количество на расценки.

[worm2]

MoonWatcher
Ну, может быть, они на одну задачу пробовали сто подходов, один из них привёл к результату и обошёлся в 200 долларов, а 99 других к результату не привели, но токены сжигали исправно.
Может быть, они тысячу задач пробовали, получилось десять, и каждая решённая обошлась в 200 долларов, а про остальные (нерешённые) ничего не написали.
Не, по-любому, дёшево получилось, я не спорю, но настолько ли дёшево?

[MoonWatcher]

worm2 в сообщении #1729749 писал(а):

Ну, может быть, они на одну задачу пробовали сто подходов, один из них привёл к результату и обошёлся в 200 долларов, а 99 других к результату не привели, но токены сжигали исправно.
Может быть, они тысячу задач пробовали, получилось десять, и каждая решённая обошлась в 200 долларов, а про остальные (нерешённые) ничего не написали.

Это был бы откровенный мухлеж. Уверен, что речь идет о стоимости ВСЕХ затраченных токенов. Собственно, OpenAI у себя в блоге так и пишет (автоперевод):

Цитата:

Общее количество токенов, необходимых для нахождения решений этих задач, составило бы примерно 2000 долларов США по курсам Sol API.

[realeugene]

mihaild в сообщении #1729660 писал(а):

Я подозреваю, что почти любой человек, если ему объяснить известный Эйнштейну диффгем и посадить в лифт, вывести ОТО не сможет. Значит Эйнштейн умел что-то еще, помимо знания диффгема и опыта поездок в лифте.

Эйнштейн очевидно решал проблему несовместимости ньютоновской гравитации с СТО, причём, плотно сотрудничая с другими физиками и математиками, в частности, переписываясь с Гильбертом, который вывел те же уравнения как пишут другим методом и чуть позже, но до публикации Эйнштейна. Уравнения Эйнштейна иногда называются уравнениями Эйнштейна-Гильберта. Разработка ОТО заняла больше 10 лет. Если бы LLM вывела ОТО на основании знаний физики и диффгеометрии того времени за пару часов, это бы означало, что она как физик-теоретик гораздо-гораздо-гораздо сильнее Эйнштейна.

-- добавлено через 33 минуты --

MoonWatcher в сообщении #1729683 писал(а):

Обе модели — и Fable, и Sol — сошлись во мнении, что результат №3 — это «Прорыв» (что объясняет, почему сотрудник OpenAI из всех выделяет именно его в своём твите
).

Тоже не могу оценить значимость для математики, но могу оценить объём доказательства: формальное доказательство на языке Lean лежит на гитхабе. Формальное доказательство этого третьего результата на языке Lean состоит из 1.4 миллиона символов, 34 тысячи строк или 1061 теоремы. Впечатляет.

[ozheredov]

realeugene в сообщении #1729787 писал(а):

Если бы LLM вывела ОТО на основании знаний физики и диффгеометрии того времени за пару часов, это бы означало, что она как физик-теоретик гораздо-гораздо-гораздо сильнее Эйнштейна.

Только Эйнштейн сам допетрил, что нужно выводить. А LLM бы подсказали (да ещё и замели 100500 неудачных попыток вывода под ковёр)

[Sender]

realeugene в сообщении #1729787 писал(а):

Формальное доказательство этого третьего результата на языке Lean состоит из 1.4 миллиона символов, 34 тысячи строк или 1061 теоремы. Впечатляет.

Б. Паскаль писал(а):

Это письмо получилось таким длинным потому, что у меня не было времени написать его короче

[realeugene]

ozheredov в сообщении #1729812 писал(а):

Только Эйнштейн сам допетрил, что нужно выводить.

Думаю, то что ньютоновская гравитация не стыкуется с СТО было всем очевидно.

[Klein]

17/08/2026
Теренс Тао
Эссе, основанное на публичной лекции, прочитанной на Международном конгрессе математиков 2026 года, посвящено тому, как математическое сообщество могло бы отреагировать на появление инструментов искусственного интеллекта, способных выполнять математические задачи исследовательского уровня.


Основное содержание
Главная мысль статьи состоит в том, что обсуждение ИИ в математике не должно ограничиваться вопросом:
«Может ли искусственный интеллект решать сложные математические задачи?»
Тао предлагает временно предположить, что в ближайшем будущем ИИ действительно сможет выполнять значительную часть исследовательской математической работы — с приемлемой точностью, стоимостью и степенью человеческого контроля. После этого возникает более глубокий вопрос:
«Для чего вообще существует математическое исследование и какие его результаты мы действительно считаем ценными?»
Автор подчёркивает, что это условное рассуждение. Он не доказывает, что сильный математический ИИ обязательно появится, а исследует последствия на случай, если это произойдёт.

https://arxiv.org/html/2608.16753v1

[MoonWatcher]

Попросил GPT-5 изложить основные тезисы статьи:

(Оффтоп)

Статья Терренса Тао «Mathematics in the Age of AI» — это не столько прогноз возможностей ИИ, сколько размышление о том, что вообще считать целью математической работы, если ИИ действительно научится решать значительную часть исследовательских задач. Тао специально принимает это как рабочую гипотезу и не пытается здесь доказать, насколько она реалистична.

### Основные тезисы

1. ИИ создаёт для математики не столько техническую, сколько ценностную проблему.
В начале XX века математика пережила кризис оснований и в результате стала более формальной и строгой. По мнению Тао, теперь начинается похожий период переосмысления — но под вопросом оказываются не основания математической истины, а наши неявные представления о том, что является хорошей математикой, ценным результатом и авторством.

2. Нельзя сводить цель математики к количеству решённых задач.
У математики множество целей: решение проблем, создание теорий, понимание мира, обучение новых математиков, развитие сообщества, накопление общего знания, создание эстетически ценных произведений и т. д. Исторически эти цели были достаточно хорошо согласованы, поэтому одну из них можно было использовать как приближённый показатель остальных.

3. ИИ может разрушить эту корреляцию из-за закона Гудхарта.
Если начать чрезмерно оптимизировать один показатель — например, число решённых задач, — он перестаёт быть хорошим показателем настоящего прогресса. ИИ особенно опасен в этом отношении: он способен очень эффективно оптимизироваться под видимость успеха, а индустрия ИИ дополнительно стимулирует benchmarkable achievements.

4. Тао постепенно расширяет понятие «решить математическую задачу».
Он показывает последовательность:

решить → проверить → объяснить → добиться принятия сообществом → встроить результат в теорию.

Простого правильного доказательства недостаточно. Даже формально проверенное доказательство может быть практически бесполезным, если его никто не понимает.

5. «Правильное, но непонятное» доказательство — серьёзная проблема.
Proof assistant вроде Lean может подтвердить корректность доказательства, созданного ИИ, но это ещё не означает, что человек понял математическую идею. Тао считает человеческое понимание существенной частью математического результата. Его довольно жёсткое правило: если авторы не способны дать ясный экспертный доклад о результате, корректно объяснив его и атрибуцию, результат не следует публиковать — даже если доказательство формально проверено.

6. Интересно, что Тао защищает даже «недостатки» человеческого математического текста.
В сложных человеческих доказательствах нередко видны места, где автор сам испытывал трудности: необычная лемма, смена обозначений, поясняющий комментарий. Эта «естественная шероховатость» показывает читателю, где находится настоящая сложность. ИИ может отполировать текст настолько хорошо, что исчезнут именно эти полезные сигналы: текст станет легче читать, но труднее учиться по нему.

7. Главная будущая проблема — не дефицит доказательств, а их избыток.
Если ИИ станет достаточно хорош, возникнет переход от proof scarcity к proof abundance:
- доказательств будет больше, чем способны проверить люди;
- проверенных доказательств — больше, чем можно нормально изложить;
- хорошо изложенных — больше, чем способны отрецензировать эксперты;
- опубликованных — больше, чем математическое сообщество способно интегрировать в теории и учебники.

8. Поэтому придётся переоценить статус математической «инфраструктуры».
Рецензирование, редактура, объяснение результатов, систематизация и включение результатов в учебники сейчас менее престижны, чем получение нового доказательства. Тао считает, что в эпоху ИИ должно произойти смещение акцента от proof generation к proof digestion — от производства доказательств к их проверке, пониманию, публикации и канонизации.

9. Человеческое авторство и ответственность должны сохраняться.
ИИ может быть инструментом, но авторство и ответственность должны оставаться за людьми. Кроме того, необходимо тщательно отслеживать происхождение идей и давать правильные ссылки: у ИИ есть проблемы с attribution.

10. Рекомендация — не запрещать ИИ, а самим формировать правила его использования.
Тао выступает за прозрачное раскрытие использования ИИ, помощь рецензентам, формализацию там, где она полезна, новые базы математических задач и новые форматы публикаций. При этом в обучении будущих математиков ИИ, вероятно, придётся ограничивать гораздо сильнее, поскольку цель обучения — не просто получить правильный ответ, а научиться думать математически.

### Если свести статью к одной мысли

Тао говорит: если ИИ действительно научится массово производить математические результаты, проблема математики перестанет быть «как получить доказательство?» и всё больше станет «какие доказательства стоит получать, как понять их смысл и как превратить огромное количество машинных результатов в человеческое математическое знание?»

И, пожалуй, самый интересный тезис статьи: математический прогресс — это не производство истинных утверждений. Это процесс превращения истинных утверждений в понятое, принятое и интегрированное сообществом знание. Именно последние этапы Тао считает наиболее ценными и наименее автоматизируемыми.

-- добавлено через 33 минуты --

Лично меня больше всего заинтересовал процитированный в статье один из принципов Лейденской декларации об искусственном интеллекте и математике:

Цитата:

Affirm the humanity of authorship
Credit and responsibility continue to belong to humans within the mathematical community and should not be given to automated systems. Artificial intelligence may obscure, but does not replace, the collective human labor behind a result.

Не совсем понятно почему ИИ, превзошедший уровень лучших математиков планеты (ну скажем, лет через 15-20), не может быть полноценным автором математических исследований и нести за них фактическую ответственность. Вероятно этот принцип следует из другого принципа, озвученного Тао в его статье:

Цитата:

A proof that no human can properly explain should be viewed as incomplete, even if it has been formally verified.

Это тоже непонятно. Чем это отличается от условного НИИ, директор которого не способен понять решение, полученное сильнейшими математиками его института? Либо Тао считает, что ИИ в принципе не способен превзойти человеческий интеллект (и лучшие математики планеты должны непременно понять любое из решений, полученных ИИ), либо это проявление иррационального антропного шовинизма.

[Mikhail_K]

MoonWatcher в сообщении #1731384 писал(а):

Это тоже непонятно. Чем это отличается от условного НИИ, директор которого не способен понять решение, полученное сильнейшими математиками его института? Либо Тао считает, что ИИ в принципе не способен превзойти человеческий интеллект (и лучшие математики планеты должны непременно понять любое из решений, полученных ИИ), либо это проявление иррационального антропного шовинизма.

Ни то ни другое. Просто для Тао математика ценна не как набор достижений (доказанных утверждений и построенных теорий), а как область человеческой культуры, в рамках которой люди разбираются в доказательствах, ценят их и обсуждают их друг с другом. Таким образом, непонятное никому из людей доказательство может быть правильным, но оно не будет относиться к математике как части человеческой культуры.

[MoonWatcher]

Математика и не должна быть частью человеческой культуры - на то она и математика, а не искусство.

[Mikhail_K]

MoonWatcher в сообщении #1731397 писал(а):

Математика и не должна быть частью человеческой культуры - на то она и математика, а не искусство.

Вы думаете, что не должна, а Тао (и далеко не он один) думает, что должна.

Кому-то математика важна как инструмент для достижения каких-то целей, для применения в каких-то областях - и с этой стороны пожалуй что да, главное в инструменте это его эффективность. Тут есть нюансы для возможного обсуждения, но в целом это так.

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