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.