Тут в адрес нашумевшего доказательства возникновения сингулярности у решений уравнений Навье-Стокса с помощью ChatGPT от OpenAI метнули научную ответочку в любимом мной стиле: https://arxiv.org/abs/2610.08144

Суть: Формальная проверка доказывает корректность формализованного рассуждения, но сама по себе не гарантирует, что при переводе в формальный язык сохранился смысл исходного доказательства. Авторы рассматривают эту проблему на примере перевода математических текстов с помощью ИИ в Lean.

Пояснение для тех, кто не в теме: поскольку на человеческом языке доказательство получилось очень большим, для ускорения верификации доказательства использовался перевод в машиночитаемый язык строгой формальной верификации Lean. И вот именно на этой трансформации самый большой семантический разрыв с исходной логикой и мог накопиться. С учетом печальной склонности ИИшечки подгона ответа под желаемое, разрыв может достигать неприемлемого отклонения, после которого вся трансформация в Lean потеряла смысл и превратилась в галлюциногенный нейрослоп.