टेरेन्स टाओ की नज़र में proof checkers और AI गणित copilot
(scientificamerican.com)- जैसे-जैसे गणितीय proofs अधिक सख्ती से formalize किए जा रहे हैं, Lean जैसे tools मानव proofs को verify कर रहे हैं और बड़े पैमाने के collaboration की भरोसे की बुनियाद बदल रहे हैं
- mathlib जैसी standard libraries के बढ़ने से undergraduate स्तर के theorems से लेकर नए क्षेत्रों तक को formalize करने की entry barrier कम हो रही है
- PFR conjecture के formalization में 20 से अधिक प्रतिभागियों ने छोटे-छोटे proof steps बाँटकर संभाले, और टेरेन्स टाओ ने line-by-line review के बजाय overall direction management पर ध्यान दिया
- AI अभी गणित को “solve” करने से अधिक proof copilot की तरह formalization, verification और repetitive काम में मदद करने के करीब है
- गणितीय research मानव द्वारा दिशा तय करने, detail formalization, AI training और AI proofs की interpretation जैसे अधिक explicit और division-of-labor वाले कामों में बदल सकती है
Formalization से बदलता गणितीय collaboration
- पारंपरिक गणितीय research अपेक्षाकृत छोटे collaboration पर आधारित रही है, और टाओ के अनुसार आमतौर पर लगभग 5 लोग collaboration के practical upper limit के करीब होते हैं
- अगर automatic proof checker हो, तो सैकड़ों ऐसे लोगों के साथ भी collaboration संभव है जो एक-दूसरे को नहीं जानते
- contributors code upload करते हैं, और Lean compiler उसे verify करता है
- भरोसा सिर्फ निजी संबंधों पर निर्भर नहीं रहता, बल्कि formal verification results से पुष्टि की जा सकती है
- Polynomial Freiman-Ruzsa (PFR) conjecture के हालिया result को formalize करते समय 20 से अधिक लोगों ने भाग लिया
- proof को कई छोटे steps में बाँटा गया
- हर प्रतिभागी ने एक step का proof संभाला
- टाओ ने हर contribution को line-by-line जाँचने के बजाय overall progress direction को manage किया
हर गणितज्ञ का programmer होना ज़रूरी नहीं
- formalization projects में roles बाँटे जा सकते हैं
- कुछ लोग गणितीय दिशा पर ध्यान दे सकते हैं
- कुछ लोग छोटे गणितीय हिस्सों को formal proofs में बदलने का विशेषज्ञ काम कर सकते हैं
- Peter Scholze जैसे ऐसे गणितज्ञ भी Lean projects में भाग ले सकते हैं जो computers के साथ बहुत सहज नहीं हैं
- अगर बड़े गणितीय कामों को छोटे हिस्सों में बाँट दिया जाए, तो पूरी theory समझे बिना भी कोई व्यक्ति किसी खास subtask में योगदान दे सकता है
Lean, mathlib और search से बनी practical usefulness
- formal mathematics के व्यावहारिक होने के बड़े कारणों में से एक standard mathematics libraries का विकास है
- Lean में mathlib नाम का एक बड़ा project है
- calculus, topology जैसी undergraduate mathematics की basic theorems एक-एक करके library में जोड़ी जा रही हैं
- लक्ष्य library को graduate स्तर तक ले जाना है
- ऐसा होने पर नए गणितीय क्षेत्रों को formalize करना आसान हो जाएगा
- proofs बनाने के लिए पहले से true साबित किए गए theorems खोजने पड़ते हैं, इसलिए अधिक smart search engine भी महत्वपूर्ण हो जाते हैं
- पूरे PFR project को formalize करने के बाद verification compile में केवल लगभग 30 मिनट लगते हैं
- bottleneck computing power से अधिक usability, user-friendliness और लोगों का tools के अनुकूल होना है
- Lean को इस समय सबसे सक्रिय community वाली formal language माना जाता है
- single-author projects के लिए दूसरी languages बेहतर हो सकती हैं
- Lean सीखना अपेक्षाकृत आसान है, और इसकी library व community अच्छी है
- भविष्य में इसे कोई और alternative replace कर सकता है, लेकिन फिलहाल यह dominant formal language है
अभी भी formalization की लागत ऊँची है
- टाओ के अनुसार किसी project को formalize करना संभव है, लेकिन अभी इसके लिए उन्हें अपना एक महीना लगाना पड़ सकता है
- अभी हम उस stage पर नहीं हैं जहाँ हर result को रोज़मर्रा में formalize किया जाए
- जब Lean सीखने में मदद मिलती हो
- जब result की correctness में विशेष रुचि हो
- तब ऐसे projects चुनने चाहिए जहाँ formalization वास्तव में value दे
- technology बेहतर होने पर formalization की cost कम हो सकती है
- अभी यह पारंपरिक तरीके से 10 गुना अधिक समय ले सकता है
- आगे चलकर यह लगभग 2 गुना, और फिर 1 गुने से भी कम तक आ सकता है
AI गणितज्ञ का copilot बन सकता है
- टाओ भविष्य में ऐसी स्थिति की कल्पना करते हैं जहाँ गणितज्ञ proof खुद type करने के बजाय GPT जैसे system को समझाएँ, और AI चलते-चलते Lean formalization की कोशिश करे
- verification pass हो जाए तो LaTeX paper और Lean proof साथ दिए जा सकते हैं
- अगर उपयोगकर्ता चाहे, तो यह journal submission तक में मदद करने वाला assistant बन सकता है
- अभी सबसे तेज formalization path वही है जिसमें पहले मनुष्य proof की idea और draft बनाता है
- लंबी अवधि में ऐसे projects भी संभव हो सकते हैं जहाँ मनुष्य को पूरा proof न पता हो, लेकिन छोटे हिस्सों को formalize किया जाए और AI व मनुष्य मिलकर उन्हें जोड़कर बड़ा theorem साबित करें
- टाओ के अनुसार यह संभव होने में कई साल लगेंगे
- मौजूदा technology अभी पर्याप्त नहीं है, और formalization अब भी एक painful process है
“गणित solve हो जाएगा” वाले दावे से दूरी
- Tony Wu और Christian Szegedy ने कहा है कि 2–3 साल में मशीनें proofs खोजने में मनुष्यों से बेहतर हो सकती हैं, इस अर्थ में कि गणित “solve” हो जाएगा
- टाओ मानते हैं कि 3 साल के भीतर AI गणितज्ञों के लिए उपयोगी बन सकता है और स्पष्ट प्रगति दिख सकती है, लेकिन इससे गणित solve हो गया ऐसा नहीं कहा जा सकता
- AI एक copilot की तरह मदद कर सकता है जब proof का कोई step सही लगता हो लेकिन मनुष्य उसे तुरंत न देख पा रहा हो
- अगर AI वर्तमान मानव-स्तर का गणित करने लगे, तब भी मानव गणितज्ञ और ऊँचे स्तर के गणित की ओर बढ़ सकते हैं
- AI की मदद से एक साथ सैकड़ों या हज़ारों theorems साबित करना भी संभव हो सकता है
- मानव गणितज्ञ AI को क्या करना है, यह निर्देशित करने की भूमिका निभाएँगे
- टाओ के अनुसार इस बदलाव के लिए 2–3 साल की timeline कुछ आक्रामक लगती है
proof को समझना और AI-generated proofs
- गणितीय proof सिर्फ सत्यापन की प्रक्रिया नहीं है, बल्कि यह समझने की प्रक्रिया भी है कि कोई बात सही क्यों है
- निकट भविष्य में AI पहले उबाऊ और मामूली काम automate करेगा, जबकि दिशा तय करने का काम अभी भी मनुष्यों के पास रहने की संभावना है
- अगर AI ऐसा proof दे जो समझने में कठिन और भद्दा हो, तो मनुष्य बाद में उसका फिर से analysis कर सकते हैं
- उदाहरण के लिए, अगर 10 assumptions से किसी conclusion तक पहुँचा गया है, तो यह जाँचा जा सकता है कि क्या उनमें से एक assumption हटाने पर भी proof चलता है
- AI-generated proofs से insight निकालने वाले नए तरह के गणितज्ञ उभर सकते हैं
- शुरुआती AI proofs में insight नज़र नहीं भी आए
- लोग उन proofs को अधिक समझने योग्य बनाएँगे और उनकी structure खोजेंगे
अनसुलझी समस्याएँ और AI की सीमाएँ
- किसी unresolved conjecture को साबित करने से पहले अक्सर उसे छोटे हिस्सों में तोड़ना पड़ता है
- किसी समस्या को आसान समस्या में बदलने की तुलना में उसे और कठिन समस्या में बदलना कहीं अधिक आसान है
- टाओ के अनुसार AI ने अभी तक यह क्षमता नहीं दिखाई है कि वह इस decomposition काम में मनुष्यों से बेहतर है
- AI का अलग-अलग क्षेत्रों के बीच संभावित connections सुझाना दिलचस्प है
- अभी इसकी success rate कम है
- 10 सुझावों में 1 ही दिलचस्प हो सकता है और 9 बेकार
- टाओ मानते हैं कि भविष्य में यह बदल सकता है
गणितीय ज्ञान की data problem
- mathematics AI training की एक समस्या यह है कि पर्याप्त data उपलब्ध नहीं है
- online papers training में उपयोग किए जा सकते हैं, लेकिन बहुत-सी गणितीय intuition papers में दर्ज नहीं होती
- गणितज्ञों के बीच की बातचीत
- lectures
- छात्रों को guide करने के तरीके
- असफल प्रयास और सुधार की प्रक्रिया
- published proofs compressed outputs होते हैं, और लोग आमतौर पर सिर्फ success cases ही publish करते हैं
- वास्तव में सबसे कीमती data वह process है जिसमें किसी ने कुछ कोशिश की, वह काम नहीं किया, और फिर उसे कैसे सुधारा गया
- भविष्य में research attempts और failure process को record किया जा सकता है, ताकि AI training में या दूसरे researchers को वही गलती दोहराने से बचाने में उपयोग हो सके
- टाओ 2040 के किसी advanced AI Lean-जैसे system का उदाहरण देते हैं, जिसके उपयोग के लिए researcher अपने research process records साझा करने पर सहमत हो
अधिक explicit mathematics की ओर बदलाव
- बहुत-सा गणितीय ज्ञान अलग-अलग गणितज्ञों के दिमाग में बंद है, और उसका बहुत छोटा हिस्सा ही explicit रूप में बचता है
- जैसे-जैसे formalization बढ़ेगा, implicit knowledge का बड़ा हिस्सा explicit knowledge में बदलेगा
- formalized textbooks आगे चलकर interactive textbooks बन सकते हैं
- शुरुआत high-level proof explanation से हो सकती है
- जो step समझ न आए, उसे और विस्तार से खोला जा सके
- चाहें तो axioms के स्तर तक नीचे जाया जा सके
- इस तरह एक क्षेत्र के गणितज्ञ के लिए दूसरे क्षेत्र में योगदान देना आसान हो सकता है
- बड़े काम के subtasks को सटीक रूप से define किया जा सकता है
- पूरी चीज़ समझे बिना भी ज़रूरी हिस्से में भाग लिया जा सकता है
1 टिप्पणियां
Hacker News टिप्पणियां
https://archive.is/Idouw
project manager mathematicians वाला वाक्यांश Edsger Dijkstra की 1975 में लिखी व्यंग्य रचना “A letter to my old friend Jonathan” [1] और उसके बाद के लेख [2] की याद दिलाता है
यह इस बात की आलोचना करने वाला लेख था कि software बनाने का तरीका अगर गणित पर लागू किया जाए तो वह कितना हास्यास्पद लगेगा, लेकिन एक तरह से यह दूरदर्शी भी था
मुख्य बात बौद्धिक संपदा अधिकारों, खासकर गणितीय सत्य पर बौद्धिक संपदा अधिकार लागू करने की बेतुकापन की आलोचना थी, और सौभाग्य से आज के mechanization के रुझान में वह हिस्सा बड़ी चिंता नहीं लगता
[1]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD04xx/E...
[2]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD05xx/E...
लेख insightful है, लेकिन मुझे लगता है कि इसमें छूटी हुई बात यह है कि LLM धीरे-धीरे अतिमानवीय तरीके से abstraction करने लगेंगे
Tao ने कहा कि “समस्या को कठिन बनाना आसान है, लेकिन सरल बनाना कठिन है, और AI ने कभी नहीं दिखाया कि वह इस मामले में इंसानों से बेहतर है”, लेकिन LLM के काम करने के तरीके को देखते हुए कहीं ऊंचे स्तर की insight संभव हो सकती है
अभी वे सहायक, fact-checker और उबाऊ काम निपटाने वाले जैसे हैं, लेकिन जल्द ही insight सुझाने वाली इकाई बन जाएंगे। LLM पहले से ही embeddings और knowledge को compress करते हैं और उनके पास ऐसी insights हैं जो हमें नहीं दिखतीं
Hinton का nuclear bomb और compost heap के संबंध को उदाहरण के तौर पर दिखाने वाला हिस्सा: https://www.youtube.com/watch?v=Gg-w_n9NJIE&t=4613s
वे बस ऐसी मशीनें हैं जिन्हें इंसानों के लिखने के तरीके की नकल करने के लिए train किया गया है, और इंसान से ज़्यादा बुद्धिमान किसी चीज़ की नकल करने के लिए ज़रूरी training data मौजूद नहीं है
इसमें शक नहीं कि machine learning मानव बुद्धि से आगे निकलेगी, लेकिन bottleneck यह है कि पूरी दुनिया की लिखाइयों पर regress करने के बजाय, मानव हस्तक्षेप के बिना अपने ही output से खुद को train कराने का तरीका कैसे खोजा जाए
Ramanujan ने औपचारिक शिक्षा के बिना, सिर्फ़ गणित की कुछ किताबें देखकर भी शानदार गणितीय खोजें कीं, जो machine learning model के training data के नज़रिए से लगभग कुछ भी नहीं है
उसे शब्दों में ढालने में करीब 10 सेकंड लगे, लेकिन अगर आपके पास ज़रूरी जानकारी हो तो जवाब साफ़ था
Hinton कहते हैं कि यह analogical thinking दिखाता है, लेकिन gardening से जुड़े लेख और compost heap physics की बातें online बहुत हैं, और संभव है कि ChatGPT ने training के दौरान उन्हें पहले ही देखा हो
इसलिए यह उदाहरण ऐसा लगता है जैसे LLM ने training text में असल में जवाब पहले ही देख लिया था, इस संभावना को control नहीं किया गया
वीडियो में आगे Ilya का “existence proof मौजूद है। मानव मस्तिष्क neural network है” कहना (https://youtu.be/Gg-w_n9NJIE?t=4966) भी दिलचस्प है। मैं आम तौर पर इस बात से सहमत हूं कि मानव मस्तिष्क भी neural network है, लेकिन वास्तविक neurons 8-bit पर काम नहीं करते और cell types, DNA, hormones का chemical environment आदि अलग होते हैं—ऐसे counterarguments भी बहुत हैं, इसलिए मुझे लगता है कि यहां एक दार्शनिक दोराहा है
यह कुछ मिनटों से कुछ घंटों में हो सकता है
वहीं एक और मानव expert पाने के लिए ऐसा व्यक्ति चाहिए जिसे गणित पेशे के तौर पर पसंद हो, फिर दशकों की शिक्षा और high-level specialization से गुजरना होगा, और इसकी भी guarantee नहीं कि वह अंत तक टिकेगा और ज्ञान की frontier को आगे बढ़ाने के स्तर तक पहुंचेगा
उस समय का इंतज़ार करते हुए parallel में काम करने वाले AI experts खरबों की संख्या में बनाए जा सकते हैं
मानव मस्तिष्क की नई जानकारी absorb करने की bandwidth कम है, लेकिन मशीनें जीवनभर का ज्ञान कुछ सेकंड में copy कर सकती हैं, हजारों conversations parallel चला सकती हैं, और मस्तिष्क के किसी हिस्से को serialize करके दूसरे AI को भेज भी सकती हैं। programmable matter तक पहुंचने पर computronium को exponential तरीके से बनाया जा सकता है, और कुछ सेकंड में हजारों साल का research करने जैसा omega point भी संभव हो सकता है
मुझे गणित बिल्कुल नहीं आता, लेकिन इससे software के इतिहास की याद आती है। पहले RollerCoaster Tycoon जैसे कमाल के project लगभग एक ही व्यक्ति की बनाई हुई चीज़ होते थे
उसके बाद software engineering वैसी ही modular हो गई जैसी interview में बताई गई है, और अब यह एक विशाल assembly line बन गई है जहाँ मेरे जैसे लोग रोज़ी-रोटी के लिए React उगलते रहते हैं; प्रति व्यक्ति productivity या जरूरी skill लगभग 0 के करीब लगती है
जब कोई field अपने सुनहरे दौर में होती है, तो एक genius अपने दिमाग में सौ चीज़ें रखकर बेहतरीन काम कर देता है, और जब उसकी जगह assembly line ले लेती है, तो लगता है कि वह field अब सच में valuable चीज़ें नहीं बना पाती
Software engineering ने शानदार काम करना बंद नहीं किया; मेरे हिसाब से तो ठीक उलटा हुआ है
मज़ाक अलग, किसी दिन जब कोई critical bug ठीक करना पड़ेगा, तब असली skill दिखेगी। Product या service stable और profitable हो गई है, इसका मतलब यह नहीं कि original developers जा चुके हैं या कोई बड़ा काम नहीं कर सकता
यह कहना कि यह field अब सच में valuable चीज़ें नहीं बनाती, बहुत गलत है
यह 100 लोगों द्वारा 100 साल में बनाए गए cathedral की तुलना एक व्यक्ति द्वारा एक महीने में बनाई गई झोपड़ी से करने जैसा है। झोपड़ी खड़ी रहती है और रहने की जगह देती है, लेकिन वह cathedral नहीं है
Web development में तो सिर्फ Python को भी देखें, wheel के हर छोटे cog के लिए इतने frameworks और technologies हैं कि follow करना सचमुच मुश्किल है
Skill आम तौर पर log-normal distribution follow करती है, इसलिए exceptional लोग वैसे भी कम होते हैं, और शुरुआती छोटी field में support infrastructure की कमी की वजह से सिर्फ extreme talent वाले लोग टिकते हैं, जिससे top-tier talent density अवास्तविक रूप से बहुत ऊँची हो सकती है
47 latest frameworks को जबरन जोड़कर to-do list app बनाना और meaningful impact पैदा करना बुनियादी तौर पर अलग चीज़ें हैं
Cost-benefit के लिहाज से बड़े कामों में long-term invest करने के बजाय सस्ते में बहुत सारा code उगलने की तरफ एक मजबूत local optimum होता है, और field जितनी mature होती है, उस point तक पहुँचने के लिए skill की lower bound उतनी ही कम होती जाती है
Top-tier talent को train करने पर focus करने वाले organizations भी ज्यादा नहीं हैं। इसलिए field के बड़ा होने के साथ average skill का unattended state में गिरना समझाना आसान है, और distribution को गलत handle किया गया तो बाद में उसे ठीक करना महंगा पड़ सकता है
Computer-verified proofs ऐसा area है जहाँ AI काफी निकट भविष्य में उपयोगी हो सकता है। हालांकि यह पूरी तरह LLM से ज्यादा chess engine के neural network जैसा हो सकता है
हर चीज़ को हाथ से prove करना उबाऊ और समय लेने वाला है, इसलिए पहले से ही कई solvers इस्तेमाल होते हैं, लेकिन tactics या solvers पर बहुत सारे theorems और lemmas फेंक दिए जाएँ तो वे संघर्ष करते हैं
Relevant lemmas को pattern matching से खोजने वाली search machine के रूप में neural network इस काम के लिए ठीक बैठता है
Induction और higher-order unification भी मूलतः code synthesis ही हैं, और सभी possible syntax trees को brute-force iterate करना बेहद inefficient है
Solvers तो वैसे भी backtracking करते हैं, इसलिए AI अगर 95% बेकार lemmas भी दे तो ठीक है, और manual search से नाटकीय रूप से बेहतर हो सकता है
हालांकि मुझे यकीन नहीं कि computer-verified proofs communication के लिए जरूरी तौर पर अच्छे हैं। इंसानों द्वारा पढ़े जाने वाले proofs सिर्फ लंबाई की वजह से नहीं, बल्कि कई वजहों से high-level होते हैं और details छोड़ते हैं
मुख्य समस्या यह है कि proof में इस्तेमाल होने वाली mathematical objects की formal definitions से जुड़ना पड़ता है
लेकिन इंसान proof लिखते या पढ़ते समय इस तरह नहीं सोचते। आम तौर पर उनके पास इस बात की high-level informal समझ होती है कि वे “morally” क्या कर रहे हैं, और जरूरत के मुताबिक formal details भरते हैं
Computer code में language की formal semantics mental model के कहीं ज्यादा करीब होती है, इसलिए वह कुछ हद तक काम करता है, लेकिन mathematics में आम तौर पर लक्ष्य अलग होता है
Isabelle की sledgehammer strategy E, Z3, SPASS, Vampire जैसे automated theorem provers को combine करके goal को prove या refute करने की कोशिश करती है
Theory में यह ठीक लगता है, लेकिन practice में अक्सर 12 मनमाने लगने वाले lemmas apply करके reconstructed proof मिलता है, और ऐसे proofs पढ़े नहीं जा सकते और बहुत fragile होते हैं
नहीं लगता कि AI इस problem को जादुई तरीके से solve कर देगा
मौजूदा neural networks की sample efficiency बेहद कम है, और formal mathematics datasets Python code जैसे datasets से कहीं छोटे हैं
Terence Tao ने कुछ महीने पहले इस topic पर एक शानदार talk दी थी, जिसमें Lean के उपयोग को और detail में cover किया गया है: https://www.youtube.com/watch?v=AayZuuDDKP0
एक मौजूदा गणितज्ञ ने कहा कि शोध के दौरान GPT-4o से शायद एक नया lemma सिद्ध करवाया
“मेरे पार्टनर गणितज्ञ हैं, और पिछले हफ्ते उन्होंने पहली बार ChatGPT का इस्तेमाल करके research के लिए कुछ lemmas सिद्ध करवाने की कोशिश की. उन्हें पहले से शक था कि वे theorems सही होंगे और approach भी मोटे तौर पर पता था, लेकिन वे उस तरह के propositions के specialist नहीं थे. model से सही और उपयोगी proof मिलना उनके लिए पहली बार था
पहला lemma एक collaborator ने छोटे e values पर calculation में खोजा था. ChatGPT तब तक proof नहीं ढूंढ पाया जब तक हमने उसे Möbius function इस्तेमाल करके देखने को नहीं कहा
https://chatgpt.com/share/9ee33e31-7cec-4847-92e4-eebb48d4ff...
दूसरा थोड़ा ज़्यादा standard लगता है और शायद Mathematica भी कर सकता था. लेकिन Mathematica साफ़ derivation नहीं देता, इसलिए यह फिर भी उपयोगी है
https://chatgpt.com/share/7335f11d-f7c0-4093-a761-1090a21579...”
ये चीज़ें reasoning और भारी विषयों में डरावनी हद तक अच्छी होती जा रही हैं
अगर machine learning field LLMs की लगभग System 1 thinking को complement करने के लिए System 2 capabilities जोड़ने पर ध्यान देती रही, तो हालात काफ़ी wild हो सकते हैं
यह प्रभावशाली memory है, नया reasoning नहीं
हमने इसे |τ|! coefficient वाले partition sums की बजाय ordered partitions के sum के रूप में सोचा था, लेकिन दोनों बेशक same हैं
cyclically ordered partitions, यानी |τ|! की जगह (|τ|-1)! coefficient इस्तेमाल करने पर (-1)^e नहीं बल्कि 0 आता है
Beren का combinatorial proof यह है कि एक special element चुना जाए; अगर वह element अकेला हो तो उसे अगले part से merge कर दिया जाए, और अगर अकेला न हो तो उसे उसके अपने part में split कर दिया जाए. इस तरह even length और odd length के cyclically ordered partitions के बीच bijection बनता है
linear order के case में इसी तरह last element से apply करें, लेकिन जिन partitions में last element last part में अकेला है वे match नहीं होते, इसलिए अगले element पर recursively आगे बढ़ें
अंत में सब कुछ match हो जाता है, और सिर्फ़ वही partition बचता है जिसमें हर element अलग-अलग है और original order में है. original set size की parity के हिसाब से sign sum original proposition तक ले जाता है
“τ ≤ τ” पर sum में कितने terms हैं यह भी नहीं पता, और यह Step 3 के left-hand side या right-hand side में से एक को establish करके दूसरी side conclude करने से कैसे जुड़ता है, यह भी match नहीं करता
असल में ChatGPT ने partition lattice का Möbius function याद कर लिया और proof के बिना दोहरा दिया, और उसके बाद ऊपर से plausible लगने वाली बकवास उगल दी
उस Möbius function को establish करना ही असल में core है, और सवाल लगभग उसी function के उस form में होने को prove करने जैसा है
ऊपर से ChatGPT ने जो general formula दिया वह भी थोड़ा गलत है, और सिर्फ़ |σ| = 1 वाले case में सही है, जो current proof के लिए important है
यह fact पूरे Möbius function machinery को explicit रूप से इस्तेमाल किए बिना भी तुरंत दिख सकता है: N(t,e) को t equivalence classes में बांटने वाले partitions की संख्या मानें, और recurrence N(t,e+1)=N(t-1,e)+tN(t,e) से elementary induction करें
इस interview में तीन बातें उभरकर आती हैं
पहली, Tao एक ऐसे future की कल्पना करते हैं जहां mathematical insights भी society के दूसरे outputs की तरह “produce” होंगी, और वे project manager mathematicians की बात करते हैं. उनके मुताबिक mathematics अब तक इतनी industrialize इसलिए नहीं हो पाई क्योंकि tools की कमी है, और AI व proof assistants इस हिस्से में revolutionary हो सकते हैं. हालांकि human interaction और guidance अब भी ज़रूरी है
दूसरी, papers में न आने वाला tacit knowledge बहुत ज्यादा है. intuition या failure का knowledge जैसी चीज़ें महत्वपूर्ण हैं, इसलिए top mathematicians को भी वही गलतियां दोहराने से बचने के लिए आपस में बात करनी पड़ती है
तीसरी, यह सोचना आसान है कि mathematics पहले से ही पूरी तरह formalized है, लेकिन papers में बहुत सा common knowledge assumed होता है. proofs को proof assistants के समझने लायक formalize करने से ज़्यादा लोगों को यह समझने में मदद मिलती है कि असल में क्या हो रहा है
Tao ने Polymath project के lecture में जैसा दिखाया, उससे साफ़ होता है कि वे हमेशा mathematical research के नए तरीके खोजने वाले व्यक्ति हैं
फिलहाल यह शायद ऐसा project हो सकता है जो Tao या Scholze जैसे Fields medalists के लिए संभव हो, जब वे proof पर 10 गुना समय लगाने की गुंजाइश रखते हों
हाल ही में मैंने एक top-tier math department के postdoc से बात की, और उन्होंने कहा कि उनके आसपास actual work में lean4 इस्तेमाल करने वाला कोई नहीं है
early-career researcher के लिए शायद अपनी intuition पर भरोसा करके paper publish करना बेहतर होगा
इस topic को ठीक से देखने के लिए कुछ लोगों की impressions काफी नहीं हैं
दूसरी ओर low-dimensional topology जैसे ज़्यादा intuitive style वाले fields में proof checkers इस्तेमाल करने वाले कम होंगे, ऐसा मेरा अनुमान है
यहां intuitive कहने का मतलब less rigorous नहीं है. किसी homotopy equivalence का diagram proof, inequalities की list की तुलना में Lean के समझने लायक translate करना कहीं ज्यादा मुश्किल है
reference के लिए, मैं geometry/topology side में हूं, और अब तक ऐसे tools इस्तेमाल करने वाला कोई देखा या सुना नहीं है
https://lean-lang.org/
https://github.com/leanprover/lean4
“अगर AI कोई ऐसा proof देता है जो समझ में न आने वाला और बदसूरत है, तो हम उसे लेकर analyze कर सकते हैं। अगर यह proof 10 assumptions का इस्तेमाल करके एक conclusion तक पहुँचता है, तो क्या एक assumption हटाने पर भी proof काम करता रहेगा? ऐसी science अभी मौजूद नहीं है, क्योंकि AI-generated proofs बहुत ज़्यादा नहीं हैं, लेकिन AI-generated mathematics को लेकर उसे ज़्यादा समझने योग्य बनाने वाले एक नए तरह के mathematician पैदा होंगे” — यह हिस्सा code के public API design को लेकर मेरी सोच से बिल्कुल मेल खाता है
पारंपरिक रूप से यह भूमिका सिर्फ़ अनुभवी developers निभाते थे, लेकिन अब यह काफ़ी सरल होकर सभी के लिए accessible हो सकती है