OpenAI выложила 372 AI-доказательства теорем — 25 филдсовских лауреатов бьют тревогу

OpenAI выложила в открытый доступ 372 математических утверждения, полностью сгенерированных ИИ. Результаты сопровождаются формальными доказательствами на языке Lean — это позволяет машине автоматически проверять их корректность. На каждое такое доказательство ушло в среднем около трёх часов вычислений в режиме ChatGPT Pro.

Инициатива явно бросает вызов академическому сообществу: OpenAI предлагает математикам «подтягиваться» и использовать ИИ для ускорения работы. Однако 25 лауреатов Филдсовской премии выступили с резким предупреждением. Они считают, что автоматическая штамповка теорем может уничтожить «плодородную почву» математики — ту самую неформальную интуицию и долгие размышления, из которых рождаются настоящие прорывы.