OpenAI выложила 372 математических доказательства от ИИ

OpenAI опубликовала 372 новых математических результата на GitHub, платформе для хранения кода и файлов проектов. Почти все они были сгенерированы одним ИИ-агентом по одному промпту. Каждое доказательство в среднем стоило около трёх часов вычислений ChatGPT Pro. В подборке — продвижение в гипотезе Римана, знаменитой нерешённой проблеме теории чисел, и улучшения вычислительных алгоритмов. Некоторые доказательства идут с формальной верификацией на Lean, языке программирования, который проверяет математическую логику шаг за шагом. В ответ 25 лауреатов Филдсовской премии, высшей награды в математике, подписали открытое письмо против этой практики. Они предупреждают, что поток готовых результатов без объяснений выжигает почву для новых идей, вместо того чтобы её выращивать.

Три часа вычислений модели на одно открытие — это дёшево. Часть этих результатов действительно опирается на формальную верификацию в Lean, а не только на слова агента. Но большинство из 372 результатов вышли без объяснений. Это повторяет проблему непроверенного кода, написанного ИИ. Результат может быть верным, но доверять ему без чьей-либо проверки всё равно рискованно. Формальная верификация здесь и есть настоящая проверка. Всё остальное — пока необработанный, непроверенный результат.