Математики нашли, что OpenAI формально доказала не то, что заявила словами

Математики из Кембриджа проверили код на Lean 4, которым OpenAI подтверждала своё доказательство по уравнениям Навье — Стокса, и нашли расхождение между формальной записью и словесной формулировкой. Lean — язык, в котором доказательство проверяется машиной строка за строкой, поэтому успешную проверку часто считают гарантией правильности.

Авторы работы показывают, что машинная проверка гарантирует корректность только того утверждения, которое записали на Lean, — а перевод словесной теоремы в формальную запись делала модель, и в переводе утверждение изменилось. Формально доказанным оказалось не то, что заявлено по-русски и по-английски.

Спор вокруг доказательства тянется месяц: на Хабре его описывают как 166 страниц текста, вокруг которых путаются сами математики.