MWC 2018
2018
Computex
IFA 2018
В минувшие выходные инженер-программист Нил Сомани (Neel Somani) тестировал математические способности новой модели искусственного интеллекта OpenAI и сделал неожиданное открытие. Он поставил ChatGPT сложнейшую математическую задачу, дал чат-боту подумать 15 минут и получил готовое решение.
Источник изображения: Thomas T / unsplash.com
Исследователь оценил доказательство, провёл его формализацию при помощи средства от Harmonic, и всё оказалось в порядке. Ещё больше его впечатлила цепочка рассуждений ChatGPT — в ней ИИ воспроизвёл формулу Лежандра, постулат Бертрана и теорему о звезде Давида; а также нашёл на Math Overflow сообщение от 2013 года, где приводилось решение аналогичной задачи. Окончательный вариант от ChatGPT имел существенные отличия от образца и давал полное решение версии одной из задач, поставленных легендарным математиком Палом Эрдёшем (Pál Erdős) — его коллекция нерешённых задач сейчас превратилась в полигон для ИИ.
Этот удивительный результат не уникален — модели ИИ теперь повсеместно применяются в математике: средства «глубокого исследования» OpenAI отвечают за обзор литературы, а Harmonic Aristotle производит формализацию доказательств. Модель OpenAI GPT-5.2, по словам Нила Сомани, оказалась искуснее в рассуждениях, чем предыдущие версии — они уже научились решать остававшиеся открытыми задачи, по сути, расширяя границы человеческих знаний.
Пал Эрдёш оставил после себя более тысячи гипотез, которые зафиксированы сообществом математиков в Сети — и они обнаружили, что GPT-5.2 на удивление хорошо справляется со сложнейшими математическими задачами. В период с 25 декабря 2025 года и по настоящий момент решены 15 задач Эрдёша, и в работе над 11 из них участвовал ИИ. Авторитетный математик Теренс Тао (Terence Tao) привёл восемь задач Эрдёша, в которых ИИ добился значительного прогресса; ещё в шести случаях его удалось достичь за счёт поиска и дальнейшего развития ранних исследований. Совсем без участия человека ИИ с ними пока не справился бы, но его роль становится более важной. «Таким образом, многие из этих более простых задач Эрдёша теперь с большей вероятностью могут решаться исключительно основанными на ИИ методами, чем человеческими или гибридными средствами», — делает вывод Теренс Тао.
Ещё один важный фактор — сдвиг в сторону формализации. Это трудоёмкая задача, которая упрощает проверку и расширение математических рассуждений; она не требует ни ИИ, ни даже просто компьютеров, но сейчас появились средства, которые в значительной мере упростили этот процесс. Популярным, например, стал инструмент Lean, разработанный Microsoft Research ещё в 2013 году; средство Harmonic Aristotle позволяет в значительной мере автоматизировать эту задачу. Внезапный скачок в числе решённых задач Эрдёша привёл к тому, что упоминание сервисов Aristotle или ChatGPT добавляет материалам вескости в профессиональном сообществе.
Источник:
