По предыдущей статье о проблемах свежего доказательства Навье-Стокса разбор делать не так интересно, как прожарку. Прожарка 🔥: 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