AI का Navier-Stokes प्रमाण गलत अनुवाद में?
मूल शीर्षक: Navier–Stokes Lost in Translation
यह क्यों महत्वपूर्ण है
AI-सत्यापित गणितीय प्रमाणों की विश्वसनीयता पर यह शोध पूरे क्षेत्र को पुनर्विचार के लिए मजबूर करता है।
Alexander Bastounis, Fabian Circelli और Anders C. Hansen ने 6 अक्टूबर 2026 को arXiv पर शोधपत्र प्रकाशित कर दावा किया कि OpenAI का Lean-सत्यापित Navier-Stokes प्रमाण मूल प्राकृतिक भाषा के तर्क से मेल नहीं खाता।
Cambridge और अन्य संस्थानों के तीन गणितज्ञों ने 25 पन्नों के इस शोधपत्र में Autoformalisation की एक बुनियादी सीमा उजागर की है। Autoformalisation वह प्रक्रिया है जिसमें AI किसी प्राकृतिक भाषा (NL) के गणितीय तर्क को Lean जैसी औपचारिक भाषा में अनुवाद करता है, जिसे बाद में मशीन से सत्यापित किया जा सकता है।
शोधकर्ताओं का मुख्य तर्क यह है कि गणितीय NL पाठ की अस्पष्टताओं को दूर करना — जो शब्दार्थ-सटीक अनुवाद के लिए अनिवार्य है — Solvability Complexity Index (SCI) पदानुक्रम में अनंत ऊंचाई पर है। सरल शब्दों में, यह समस्या Halting Problem (जिसका SCI = 1 है) से भी अधिक जटिल है, यानी किसी भी कम्प्यूटेशनल साधन से इसे हल करना असंभव है।
इस सैद्धांतिक दावे को ठोस उदाहरणों से पुष्ट करते हुए लेखकों ने कई मामले दिखाए हैं जहाँ AI ने NL कथनों और प्रमाणों का Lean में गलत अनुवाद किया। इनमें OpenAI द्वारा घोषित Navier-Stokes समीकरणों के समाधान के 'blow-up' का प्रमाण सबसे प्रमुख है। शोधपत्र स्पष्ट रूप से कहता है कि Lean में सत्यापित प्रमाण और NL में दिया गया blow-up का तर्क एक-दूसरे के अनुरूप नहीं हैं।
यह शोध AI-जनित गणित के स्वचालित सत्यापन पर बढ़ती निर्भरता पर सीधा सवाल खड़ा करता है।