Summary
University of Cambridge mathematicians report OpenAI’s natural-language Navier-Stokes proof and its Lean formalization diverge (Lemma 8.6: m+4 vs m+5), raising questions about AI auto-formalization as a substitute for peer review without invalidating the claimed solution.
Source Analysis
Research Notes
Additional sources
- 2026-10-09-navier-stokes-lean-mismatch-arxiv (Cambridge preprint)
- New Scientist Oct 8 (pipeline primary)
- DAMTP PDF mirror (authors)
Verified
- Lemma 8.6: NL bound uses m+4 derivatives; cited Lean uses m+5 (weaker).
- Authors argue faithful NL→Lean translation is formally hard (SCI hierarchy).
Unverified
- Whether NL blow-up proof is mathematically correct — explicitly not adjudicated.
Formalization error ≠ mathematical refutation.
Context
Stress-tests marketing of “Lean-verified” AI math; complements Sep 2026 navier-stokes-millennium-problem controversy.
Related wiki
openai, ai-autoformalization, lean-formalization, navier-stokes-millennium-problem, ai-for-mathematics
Draft Article
Cambridge ekibi: OpenAI Navier–Stokes Lean çevirisi PDF ile uyuşmuyor
Cambridge ve King’s College matematikçileri, OpenAI’nin Navier–Stokes doğal dil ispatı ile Lean formalizasyonunun Lemma 8.6’da ayrıştığını bildiriyor: PDF m+4 türev sınırı kullanıyor, Lean artefaktı m+5 ile daha zayıf bir estimate üretiyor. Bu, otomatik formalizasyon kalite kontrolü meselesi — ispatın matematiksel yanlışlığı iddiası değil.
Ana Gelişme
arXiv preprint “Navier–Stokes lost in translation” (Bastounis, Circelli, Hansen ve diğerleri), doğal dil → Lean çevirisinin pazarlama dilindeki “doğrulandı” iddiasını sorguluyor. SCI hiyerarşisi argümanı: NL belirsizliklerini sadık çeviri için çözme problemi, Halting probleminden formel olarak daha zor sınıfta.
Örnek 3.1: OpenAI NL makalesindeki (8.19) torus türev sınırı m+4 girdi türevi; commit f9e8bc5 Lean kodu m+5 kullanıyor. Fourier serisi yolunda üs 4 ile uyumsuzluklar listeleniyor.
OpenAI, New Scientist’e NL hatalarını düzelteceğini ve formalizasyon çalışmasına devam edeceğini söyledi.
Neden Önemli?
Lean formalizasyon ve AI for mathematics trendinde, formal checker’ın geçtiği kod parçası ile insan okuduğu teorem metni arasında faithful translation garantisi yok. Mühendislik ekipleri için paralel: LLM çıktısını testten geçirmek, iddiayı doğrulamak değildir.
Formalizasyon hatası, Navier–Stokes çözüm iddiasının matematiksel çürütmesi değildir; makale açıkça bunu ayırıyor.
Bağlam
Eylül 2026 navier-stokes-millennium-problem tartışmalarına ek katman; ai-benchmarks ve güven pazarlaması bağlamında okunmalı.
Sonraki Adımlar
OpenAI Lean commit güncellemeleri ve bağımsız matematik topluluğu incelemesi izlenecek; peer review ve formal check ayrı süreçler olarak kalıyor.