---
format: "aidr-story-markdown/v1"
id: "d9ae5a9e80693cef139c5eb0b68f25516019cd858d06e5fe70ba7d054a6fa848"
canonical_url: "https://aidr.today/d9ae5a9e?lang=en"
title: "Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs"
lang: "en"
requested_lang: "en"
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: "A report argues that Lean verification of AI autoformalisation does not guarantee correct natural language proofs due to semantic translation difficulties. The author claims that OpenAI's announced Navier-Stokes proof contains a mismatch between the natural language proof and its formalised Lean version."
---

# Navier\-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs

> [Open the canonical story](<https://aidr.today/d9ae5a9e?lang=en>)

**Published:** 2026-10-08T17:16:42.000Z
**Category:** Research
**Topics:** openai, llm, reasoning

## Summary

A report argues that Lean verification of AI autoformalisation does not guarantee correct natural language proofs due to semantic translation difficulties\. The author claims that OpenAI's announced Navier\-Stokes proof contains a mismatch between the natural language proof and its formalised Lean version\.

## Sources

- [Story source](<https://arxiv.org/abs/2610.08144>)
- [Discussion](<https://lobste.rs/s/axmhji/navier_stokes_lost_translation_why_lean>)
- [Story source](<https://techcrunch.com/2026/10/08/openais-math-solutions-arent-meeting-the-fields-standards-yet/>)