--- format: "aidr-story-markdown/v1" id: "d9ae5a9e80693cef139c5eb0b68f25516019cd858d06e5fe70ba7d054a6fa848" canonical_url: "https://aidr.today/d9ae5a9e?lang=vi" title: "Navier-Stokes mất đi trong bản dịch: Vì sao việc kiểm chứng Lean đối với autoformalisation của AI không đảm bảo chứng minh ngôn ngữ tự nhiên chính xác" lang: "vi" requested_lang: "vi" available_langs: ["en","vi"] translation_fallback: null fallback_fields: [] published_at: "2026-10-08T17:16:42.000Z" category: "Research" topics: ["openai","llm","reasoning"] source_urls: ["https://arxiv.org/abs/2610.08144","https://lobste.rs/s/axmhji/navier_stokes_lost_translation_why_lean","https://techcrunch.com/2026/10/08/openais-math-solutions-arent-meeting-the-fields-standards-yet/"] summary: "Autoformalisation ngày càng được dùng để kiểm chứng các văn bản toán học, gồm cả văn bản do AI tạo ra, như thông báo của OpenAI về việc chứng minh sự bùng nổ của nghiệm phương trình Navier-Stokes. Trong quá trình này, hệ thống AI dịch văn bản từ ngôn ngữ tự nhiên sang ngôn ngữ hình thức như Lean. Khi dịch xong, lập luận diễn đạt bằng ngôn ngữ hình thức có thể dễ dàng được máy móc kiểm chứng. Mục đích của bài viết này là chỉ ra vì sao quy trình đó có thể không mang lại độ tin cậy đối với lập luận ngôn ngữ tự nhiên ban đầu, do nhiều khó khăn trong việc thực hiện bản dịch chuẩn xác về mặt ngữ nghĩa. Đặc biệt, chúng tôi nhấn mạnh rằng bài toán giải quyết sự mơ hồ trong văn bản ngôn ngữ tự nhiên toán học vốn cần thiết để cung cấp bản dịch chuẩn xác về mặt ngữ nghĩa, lại nằm ở mức độ tùy ý cao trong phân cấp Solvability Complexity Index (SCI) hoặc phân cấp số học (SCI = $\\infty$). Do đó, hiểu một cách nôm na, việc cung cấp AI autoformalisation chuẩn xác về mặt ngữ nghĩa còn khó hơn bất kỳ bài toán tính toán nào, kể cả Halting problem (có SCI = 1). Để làm nổi bật tác động của kết quả này, chúng tôi đưa ra một số ví dụ về việc AI dịch sai các nhận định và chứng minh ngôn ngữ tự nhiên sang…" --- # Navier\-Stokes mất đi trong bản dịch: Vì sao việc kiểm chứng Lean đối với autoformalisation của AI không đảm bảo chứng minh ngôn ngữ tự nhiên chính xác > [Open the canonical story]() **Published:** 2026-10-08T17:16:42.000Z **Category:** Research **Topics:** openai, llm, reasoning ## Summary Autoformalisation ngày càng được dùng để kiểm chứng các văn bản toán học, gồm cả văn bản do AI tạo ra, như thông báo của OpenAI về việc chứng minh sự bùng nổ của nghiệm phương trình Navier\-Stokes\. Trong quá trình này, hệ thống AI dịch văn bản từ ngôn ngữ tự nhiên sang ngôn ngữ hình thức như Lean\. Khi dịch xong, lập luận diễn đạt bằng ngôn ngữ hình thức có thể dễ dàng được máy móc kiểm chứng\. Mục đích của bài viết này là chỉ ra vì sao quy trình đó có thể không mang lại độ tin cậy đối với lập luận ngôn ngữ tự nhiên ban đầu, do nhiều khó khăn trong việc thực hiện bản dịch chuẩn xác về mặt ngữ nghĩa\. Đặc biệt, chúng tôi nhấn mạnh rằng bài toán giải quyết sự mơ hồ trong văn bản ngôn ngữ tự nhiên toán học vốn cần thiết để cung cấp bản dịch chuẩn xác về mặt ngữ nghĩa, lại nằm ở mức độ tùy ý cao trong phân cấp Solvability Complexity Index \(SCI\) hoặc phân cấp số học \(SCI \= $\\infty$\)\. Do đó, hiểu một cách nôm na, việc cung cấp AI autoformalisation chuẩn xác về mặt ngữ nghĩa còn khó hơn bất kỳ bài toán tính toán nào, kể cả Halting problem \(có SCI \= 1\)\. Để làm nổi bật tác động của kết quả này, chúng tôi đưa ra một số ví dụ về việc AI dịch sai các nhận định và chứng minh ngôn ngữ tự nhiên sang… ## Sources - [Story source]() - [Discussion]() - [Story source]()