Navier–Stokes Lost in Translation

arXiv에 올라온 이 논문은 AI 자동 형식화(autoformalisation)가 수학 논증을 검증해 준다는 기대에 의문을 제기해요. 자연어 증명을 Lean 같은 형식 언어로 옮기면 기계적으로 검증할 수 있지만, 번역이 의미를 충실히 옮기지 못하면 원래 논증에 대한 확신은 생기지 않는다는 거예요. 저자들은 수학 자연어의 모호성을 해소하는 문제가 Solvability Complexity Index(SCI) 위계에서 SCI=∞에 해당해, 정지 문제(SCI=1)보다도 어렵다고 주장해요. 실제 AI 오역 사례도 여럿 제시하는데, 그중에는 OpenAI가 발표한 나비에–스토크스 방정식 해의 폭발(blow-up) 증명도 있어요. 논문은 이 증명의 Lean 형식화가 자연어 증명과 대응하지 않는다고 지적해요.