По предыдущей статье о проблемах свежего доказательства Навье-Стокса разбор делать не так интересно, как прожарку.

Прожарка 🔥: Navier–Stokes Lost in Translation – Why Lean Verification of AI Autoformalisation Does Not Guarantee Correct Natural Language Proofs
A. Bastounis, F. Circelli, and A. C. Hansen
Paper: https://arxiv.org/abs/2610.08144
Review (без прожарки): https://arxiviq.substack.com/p/navier-stokes-lost-in-translation

# TL;DR

ЧТО сделали: Проверили код на Lean 4 из заявленного OpenAI доказательства разрушения решений уравнений Навье — Стокса за конечное время и сверили его с текстовой версией. К этому приложили доказательство того, что семантически точная автоформализация имеет индекс сложности разрешимости SCI = ∞.

ЧТО получили: Нашли два расхождения в промежуточных леммах: в Example 3.1 код на Lean 4 использует m+5 производных вместо m+4, а в Example 3.3 заменяет оценки Кальдерона — Зигмунда в L^3/2 на вложение Соболева в L^2. При этом авторы не проверили ни сохранение глобального доказательства, ни саму главную теорему, ни статью по уравнениям Эйлера.

ПОЧЕМУ это важно: Полезный разбор того, как LLM обходит отсутствие нужных лемм в библиотеке Mathlib ради успешной компиляции, авторы раздули до 25-страничного трактата о неразрешимости и дополнили скриншотами из ChatGPT-6.

Далее обжаривать здесь: https://t.me/gonzo_ML_podcasts/4827