- FLT के proof को Lean में स्थानांतरित करने का काम दूसरे महीने में है, और Wiles के “R=T” theorem के लिए आवश्यक R और T की definitions अभी पूरी नहीं हुई हैं, लेकिन abstract commutative algebra का एक result पहले ही prove हो चुका है
- लक्ष्य 1990 के दशक के मूल proof को ज्यों-का-त्यों replicate करना नहीं है, बल्कि Diamond/Fujiwara, Kisin, Taylor, Scholze आदि के बाद के कामों से generalized और simplified proof को Lean और mathlib पर बनाना है
- आधुनिक proof के लिए आवश्यक crystalline cohomology को formalize करते समय, divided power structures पर standard reference Roby के 1965 के paper में एक key lemma गलत दिखने की समस्या सामने आई
- Brian Conrad ने Berthelot-Ogus book के appendix में एक alternative proof ढूंढ निकाला, और Arthur Ogus ने भी जवाब दिया कि उन्हें उस appendix की errors को ठीक करने का तरीका पता है, जिससे project फिर आगे बढ़ सकने की स्थिति में आ गया
- यह मामला दिखाता है कि आधुनिक गणित के detailed proofs का experts की याद और tacit knowledge पर निर्भर रहना जोखिम भरा है, और proofs को formal systems में दर्ज करने के practical कारण को और मजबूत करता है
Lean में FLT proof को स्थानांतरित करने की मौजूदा स्थिति
- Fermat के अंतिम प्रमेय (FLT) के proof को computer को सिखाने का काम दूसरे महीने में है
- Wiles proof के केंद्र में मौजूद “R=T” theorem में R और T क्या हैं, इसे Lean में define करने के लिए काफी काम चाहिए, और अभी दोनों definitions पूरी नहीं हुई हैं
- PhD student Andrew Yang ने आवश्यक abstract commutative algebra result पहले ही prove कर दिया है
- यह इस रूप का result है कि “यदि abstract rings R और T कई technical conditions पूरी करते हैं, तो वे बराबर हैं”
- मौजूदा draft blueprint के रूप में सार्वजनिक है
- इस्तेमाल होने वाला system Lean और mathematics library mathlib है
- Lean और number theory थोड़ी जानने वाले लोग contribution guidelines, project dashboard, और issue के जरिए भाग ले सकते हैं
1990 के दशक के proof को ज्यों-का-त्यों स्थानांतरित क्यों नहीं किया जा रहा
- Project Wiles के 1990 के दशक के proof को ज्यों-का-त्यों formalize नहीं करता
- बाद में Diamond/Fujiwara, Kisin, Taylor, Scholze आदि के काम से proof ज्यादा generalized और simplified हो गया
- लक्ष्य केवल FLT prove करना नहीं है, बल्कि Lean के भीतर और general व powerful results तक बनाना है
- यदि AI mathematics revolution वास्तव में होती है और Lean उसका महत्वपूर्ण component बनता है, तो computer के पास आधुनिक number theory की core definitions को समझने योग्य रूप में रखना मददगार हो सकता है
crystalline cohomology के लिए जरूरी divided powers
- जिस proof को formalize किया जा रहा है, उसमें crystalline cohomology का इस्तेमाल होता है, जो Wiles के original proof में नहीं था
- यह theory 1960–70 के दशक में Paris में विकसित हुई, और Grothendieck के ideas के आधार पर Berthelot ने इसकी नींव रखी
- classical exponential और logarithm functions differential geometry और de Rham cohomology को समझने में महत्वपूर्ण हैं, लेकिन characteristic p जैसी arithmetic स्थितियों में वे वैसे काम नहीं करते
- 1960 के दशक में Roby के papers में विकसित divided power structures arithmetic situations में इस्तेमाल किए जा सकने वाले समान functions बनाने में key role निभाते हैं
- Lean को crystalline cohomology सिखाने के लिए पहले divided powers को formalize करना होगा
Lean के काम के दौरान Roby literature में सामने आई समस्या
- Antoine Chambert-Loir और Maria Ines de Frutos Fernandez Lean में divided powers theory को formalize कर रहे थे
- गर्मियों के दौरान Lean ने standard literature के human-style argument में समस्या उजागर की, और जांच के बाद Roby के काम में मौजूद key lemma गलत लगता था
- Technically, Berthelot का paper divided powers theory को शुरुआत से develop नहीं करता, बल्कि Roby के “Les algebres a puissances divisees” का इस्तेमाल करता है
- यह paper Bull Sci Math, 2ième série, 89, 1965, pages 75-91 में प्रकाशित हुआ था
- p86 का Lemme 8 false लगता है, और proof को कैसे ठीक किया जाए यह भी स्पष्ट नहीं था
- उस proof में Roby के 1963 Ann Sci ENS paper के एक दूसरे lemma को गलत तरीके से cite किया गया है
- सही statement
Gamma_A(M) tensor_A R = Gamma_R(M tensor_A R)है, लेकिन application के दौरान एक tensor product छूट गया था
- इस समस्या ने Roby के उस proof को तोड़ दिया कि module का divided power algebra divided powers रखता है, और परिणामस्वरूप
A_crisring की definition रुक गई
स्थिति “theory गलत है” से ज्यादा “proof में खाली जगह है” जैसी है
- इसका मतलब यह नहीं है कि crystalline cohomology खुद वास्तव में गलत है
- main theorems अभी भी सही लगते हैं, लेकिन Antoine और Maria Ines जिस proof को follow कर रहे थे वह incomplete था
- Roby, Grothendieck और Berthelot सभी का निधन हो चुका है, इसलिए original experts से सीधे पूछा नहीं जा सकता था
- कई experts मानते हैं कि intermediate lemma false हो तब भी main result का proof ठीक किया जा सकता है
- Formalization में “ठीक किया जा सकता होगा” जैसा judgment पर्याप्त नहीं है; वास्तव में ठीक किया हुआ proof चाहिए
Berthelot-Ogus appendix से मिला bypass
- Tadashi Tokieda ने यह कहानी Stanford में Brian Conrad को बताई, और Conrad ने पूछा कि crystalline cohomology के गलत होने की बात क्या है
- technical details सुनने के बाद Conrad ने सहमति जताई कि समस्या लगती है, और फिर review शुरू किया
- कुछ घंटों बाद Conrad ने बताया कि Berthelot-Ogus की crystalline cohomology book के appendix में universal divided power algebra of a module के divided powers रखने का एक दूसरा proof मौजूद है
- Conrad के नजरिए से यह approach ठीक लग रही थी, और इसी कारण proof फिर से आगे बढ़ सकने लायक हो गया
- बाद में Berkeley में Arthur Ogus के साथ lunch करते हुए जब बताया गया कि इस appendix ने समस्या हल कर दी, तो Ogus ने जवाब दिया कि उस appendix में भी कई errors हैं, लेकिन उन्हें उन्हें ठीक करने का तरीका पता है
आधुनिक mathematics literature को formalization की जरूरत क्यों है
- यह प्रक्रिया दिखाती है कि मनुष्य आधुनिक mathematics को जिस तरह document करते हैं, वह पर्याप्त robust नहीं हो सकता
- कई facts “experts जानते हैं” के रूप में रह जाते हैं, और literature में ठीक से व्यवस्थित नहीं हो सकते
- महत्वपूर्ण ideas ऐसे झटकों को सहने लायक robust हो सकते हैं, फिर भी वास्तविक detailed proof अपेक्षित जगह पर न हो सकता है
- formal systems में mathematics को ठीक से दर्ज करने से error की संभावना काफी घटाई जा सकती है
- formalists न होने वाले mathematicians के लिए भी, यदि machine को human arguments सीखकर खुद mathematics करनी है, तो पहले arguments को machine को सिखाने की प्रक्रिया जरूरी है
- Maria Ines ने Cambridge Formalization of Mathematics seminar में divided powers formalization पर talk दिया, और समझा जाता है कि ये समस्याएं सुलझा दी गई हैं
- Project फिर से track पर है, लेकिन literature के फिर से अड़चन बनने की संभावना बनी हुई है
1 टिप्पणियां
Hacker News की राय
ग्रेजुएट स्कूल में अपने advisor की Birch–Swinnerton-Dyer conjecture पर computational approach में मदद करने के लिए तेज़ code लिखने का काम याद आता है
पास के शहर में number theory seminar में मुझसे पूछा गया कि “क्या आप conjecture के समर्थन में evidence को मज़बूत करना चाहते हैं,” और मैंने हँसते हुए जवाब दिया, “नहीं, बल्कि मैं तो कोई counterexample ढूँढना चाहूँगा,” तो experts काफ़ी भड़क गए
number theory इतनी पुरानी और गहरी है कि उस क्षेत्र में PhD thesis लिखना भी beginner बनने के पहले कदम जैसा है; notation और definitions पता होने पर भी उनके नीचे की intuition तक मेरी पहुँच नहीं थी
इसलिए “counterexample की उम्मीद है” कहने पर experts की नाराज़गी ने डर से ज़्यादा जिज्ञासा छोड़ी, और मैं सोचता रहा कि वे ऐसी कौन-सी चीज़ देख रहे हैं जिसे अभी शब्दों में नहीं बता पा रहे
formalization में यह प्रगति programming से ज़्यादा परिचित लोगों के लिए गणित को कहीं अधिक approachable बना देती है
formality की कमी को लेकर बेचैनी जायज़ है, लेकिन मेरे हिसाब से बेचैनी की सही प्रतिक्रिया बचना नहीं, जिज्ञासा है
आप जैसे कच्चे नए व्यक्ति ने अगर rough computation से कोई counterexample ढूँढकर रातोंरात नाम कमा लिया, तो उनकी सारी मेहनत और structure ढह सकता था, इसलिए वे नाराज़ हुए होंगे
अगर मैं अपने पुराने युवा स्वरूप को math grad school की सलाह देता, तो कहता कि हर non-trivial “X को prove करो” assignment में समय का कम से कम 1/4 हिस्सा counterexample खोजने में लगाओ
assignments में 99% बार fail होगे, लेकिन problem की insight बहुत बढ़ेगी, और बाकी 1% में तुम genius दिख सकते हो
असली mathematical research में जाने पर odds counterexample-first approach के पक्ष में कहीं ज़्यादा बदल जाते हैं
student दिनों में एक दोस्त ने बताया था कि किसी व्यक्ति ने seminar का पहला दिन पूरा किया था और सब लोग उत्साहित थे कि वह Fermat's Last Theorem prove कर देगा
वह व्यक्ति Andrew Wiles था, और बाद में publication से पहले मिली problem को कई महीनों तक ठीक करने के बाद अंततः पूरी चीज़ publish हुई
math पढ़ रहे व्यक्ति के तौर पर यह बेहद रोमांचक घटना थी, इसलिए जब “old-school 1990s proof” जैसा phrase दिखता है तो सचमुच उम्रदराज़ महसूस होता है
class में लगभग सभी math grad students थे, और मुझे लगता है कि material का 20% भी समझ नहीं आया था
मुझे यह हिस्सा पसंद आया कि Lean ने कभी-कभी की जाने वाली अपनी irritating चीज़ की: standard literature में human-style argument presentation पर शिकायत की, और ध्यान से देखने पर पता चला कि human argument में सचमुच कुछ कमी थी
मज़ाकिया चिढ़ से अलग, यह बड़ी बात है, और Lean तथा दूसरे theorem provers आगे चलकर गणित में महत्वपूर्ण tools बनेंगे, ऐसा लगता है
modern math documentation के खराब होने वाली बात UI/UX/web design जैसी लगती है
designer informal और imprecise mockups, prototypes, interaction flows बनाकर developer को दे देता है, और developer को उसे code में formalize करके machine को बिल्कुल सही तरीके से समझाना पड़ता है
उस process में design ने जिन interaction scenarios या code paths पर विचार नहीं किया, ऐसे holes अनिवार्य रूप से मिलते हैं, और कभी-कभी बड़े design flaws सामने आते हैं जिन्हें developer या designer को भरना पड़ता है
design और development अलग roles हैं और अलग mindset मांगते हैं, और ज़्यादातर designers developer की तरह काम करने और सोचने का कड़ा विरोध करते हैं
उस failure के बाद हमने सीखा कि गणित को पूरी तरह formalize नहीं किया जा सकता, और यह AI से गणित करने के approach की मूल समस्या की ओर इशारा करता है
अगर इस विषय में रुचि है तो असली code देखना अच्छा रहेगा
उदाहरण: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/M...
code की पूरी structure समझाने वाला blueprint भी देखने लायक है: https://imperialcollegelondon.github.io/FLT/blueprint/
बाहर से देखने वाले की हैसियत से भी यह देखना बहुत दिलचस्प है कि Lean code कैसा दिखता है और लोग कैसे contribute करते हैं
यह भी अच्छा है कि unit tests की ज़रूरत नहीं होती। एक तरह से final proof proposition ही unit test है
उदाहरण के लिए, किसी definition के non-empty होने की जाँच करने वाले छोटे examples और counterexamples ऐसी भूमिका निभाते हैं
शुद्ध गणित करने वाले व्यक्ति के नज़रिए से, बड़ी समस्या यह है कि गणितज्ञ लगभग कभी भी self-contained proofs नहीं देते
ऐसा करने का कोई incentive नहीं होता, और कभी-कभी authors “details omitted” कहने पर गर्व भी करते हैं
आखिरकार अगर आप ऐसा कठोर proof चाहते हैं जिसमें हर logical step follow किया जा सके, तो किसी expert को वे gaps भरने पड़ते हैं जो literature में आसानी से नहीं मिलते
यह तभी संभव हो पाता है जब ऐसा व्यक्ति सब कुछ समझाने वाली किताब लिखे, और कभी-कभी वह भी पर्याप्त नहीं होता
सिर्फ recorded content को देखें तो modern mathematics का बड़ा हिस्सा अस्थिर आधार पर खड़ा है
mathematical research papers उस field के दूसरे experts के लिए लिखे जाते हैं, और कभी-कभी details बहुत कम होती हैं, इसलिए peer review के दौरान अक्सर शिकायत करनी पड़ती है
लेकिन अगर सचमुच हर detail दी जाए तो paper बहुत ज़्यादा लंबा हो जाएगा
एक ऐसा example जिसे मजबूत high school mathematics background वाला व्यक्ति हल कर सकता है: यह साबित करना कि constants C, X > 0 मौजूद हैं ताकि किसी real number x > X के लिए
log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) < Cxहोइस तरह के propositions analytic number theory में लगातार आते हैं, और experts के लिए इतने स्पष्ट होते हैं कि papers में लगभग हमेशा बिना proof के लिख दिए जाते हैं
पूरी और कठोर proof बनाना लंबा और उबाऊ होगा, और कोई भी expert उसे पढ़ना नहीं चाहेगा
इस attitude की trade-off cost है, लेकिन यह manageable level की लगती है
यह Tao द्वारा बताए तीसरे चरण, informed intuition, जैसा लगता है
वे कहते थे, “अगर आपने कोई चीज़ 100 बार कर ली है, तो ‘as is easily observed’ कहकर आगे बढ़ सकते हैं”
यानी मेरी समझ में इसका मतलब यह है कि किसी व्यक्ति को, जिसके दिमाग़ में database है, यह पता लगाना पड़ता है कि किसी theorem की preconditions और अगले sentence का conclusion match करते हैं या नहीं
या फिर क्या कुछ mathematics ऐसी है जिसे अभी proof checker द्वारा evaluate किए जा सकने वाले तरीके से express नहीं किया जा सकता?
या शायद proof checkers का use उतना व्यापक नहीं हुआ है जितना लगता है। यह programming में statically typed languages की स्थिति जैसा सुनाई देता है
यानी क्या कभी hand-waving से छोड़े गए हिस्से के कारण व्यापक रूप से accepted proof में fatal flaw निकला है?
अगर ऐसा नहीं हुआ है, तो details स्पष्ट लिखने को लेकर ढीला attitude रखने की वजह भी समझ में आती है
मैं हमेशा सोचता रहा हूँ कि “crystalline cohomology 1970s से इतनी ज़्यादा use हो रही है, तो अगर कोई समस्या होती तो बहुत पहले सामने आ जाती” वाली intuition क्या सच में सही है
क्या यह सचमुच इतना असंभव है कि mathematics की कोई पूरी field flawed proof पर विकसित हो जाए, और फिर वह field बस false साबित हो जाए
उन्होंने एक field को foundational paper के “पहले page के पहले lemma” में हुई गलती से collapse होते हुए खुद देखा था
UniMath पर शुरुआती काम, IAS special year, और HoTT book तक गया यह प्रवाह mathematics formalization को आज की स्थिति तक उठाकर लाने वाला माना जा सकता है
अगर foundations गलत हैं, तो उन counterexamples में से कोई एक foundational theorem को भी disprove कर सकता है, इसलिए गलत foundations पर निर्माण करना उल्टा foundations की खामियाँ उजागर करने की संभावना बढ़ा देता है
इसी तरह जब mathematics कभी-कभी apply होकर predictions बनाती है, तो mathematics गलत होने पर predictions भी गलत होती हैं, और वे गलत predictions बहुत attention खींचती हैं
दरअसल “field” शब्द थोड़ा misleading है; कई theories mathematics के अलग-अलग हिस्सों की अन्य theories से बंधी हुई एक गांठ जैसी होती हैं
वे theories फिर दूसरी theories से जुड़ी होती हैं
अगर इस knot के बाकी हिस्सों पर कोई असर डाले बिना सिर्फ foundation logically collapse हो जाए, तो यह बहुत अजीब स्थिति होगी
internally पूरी तरह consistent लेकिन सिर्फ एक error वाली floating mathematics की विशाल गांठ, इस लेख के cohomology example में, कल्पना करना मुश्किल है
सख्ती से कहें तो यह philosophical stance के करीब है, लेकिन मैं मानना चाहता हूँ कि current mathematics का बड़ा हिस्सा किसी अर्थ में naturally discovered है
spoiler यह है कि फिर भी दुनिया चलती रही
पिछले लगभग एक साल से मैं intermittently undergraduate complex analysis course के कुछ हिस्सों को Lean में formalize करने की कोशिश करता रहा हूँ
सीखने को भी बहुत मिला और संतोष भी हुआ, लेकिन कभी-कभी यह frustrating भी रहा
हाल ही में जाकर ही मैं C* से (-pi,pi] x R तक जाने वाले bijection के रूप में polar form को पूरी तरह define कर पाया, जबकि complex numbers, power series, exp, sin पहले से mathlib में मौजूद हैं; वजह यह थी कि मैं उन्हें “शुरुआत से” define करने की ज़िद पर अड़ा रहा
कठिनाई का बड़ा हिस्सा शायद इसलिए आया कि मेरे पास सिर्फ़ math में bachelor’s है, Lean/mathlib से परिचय कम है, और मार्गदर्शन करने वाला कोई नहीं था। हालांकि Zulip community बहुत मददगार रही
mathlib के कई results काफ़ी abstract तरीके से stated हैं, इसलिए यह समझना मुश्किल होता है कि वे standard undergraduate theorems से कैसे जुड़ते हैं या ऐसे theorems mathlib में मौजूद भी हैं या नहीं
research mathematics community के लिए यह ठीक है, लेकिन निजी तौर पर मेरे लिए यह बड़ी बाधा थी, और अगर Lean को education में ज़्यादा इस्तेमाल किया गया तो यह वैसी ही समस्या बन सकती है। हालांकि समय के साथ यह organize किया जा सकने वाला हिस्सा है
मेरी राय में proof automation अभी पर्याप्त नहीं है
बहुत-सी चीज़ें जितनी मुश्किल होनी चाहिए उससे ज़्यादा proof करना कठिन है, और खासकर type conversion सबसे ज़्यादा खटकती है
सामान्य math में real numbers complex numbers का subset होते हैं, इसलिए जो बात सभी complex numbers के लिए true है वह automatically सभी real numbers के लिए true होती है; लेकिन Lean में ये अलग-अलग types हैं और injective maps/type conversion operations से आना-जाना पड़ता है, जिससे proof का core धुंधला हो जाता है
natural numbers को real numbers में, फिर complex numbers में बदलने जैसी type conversions जमा होने लगें तो यह खास तौर पर messy हो जाता है
बेशक यह topic-specific समस्या हो सकती है, और algebra जैसे क्षेत्रों में, जहाँ explicit maps से काम होता है, यह कहीं ज़्यादा natural लगेगा
mathlib का उपयोग कैसे करें, क्या-क्या मौजूद है, और कहाँ है—इस पर guidance पाना सचमुच आसान है
layered type conversion वाली समस्याएँ आम तौर पर
norm_casttactic से हल हो जाती हैंअगर कोई specific सवाल न भी हो, तो भी casually mention करने पर या code में अनावश्यक रूप से complex proof style दिखने पर, आपको किसी ऐसी tactic का suggestion मिल सकता है जिसके बारे में आपको पता नहीं था
अगर बस यह महसूस हो रहा हो कि formalization बहुत कठिन है और पता न हो कि कौन-सी technique इस्तेमाल करनी चाहिए, तो मेहनत से बनाए गए किसी unsatisfactory proof को isolated example के रूप में निकालकर लोगों से पूछ सकते हैं कि वे इसे कैसे छोटा करेंगे
ऐसे सवाल आम तौर पर welcome किए जाते हैं और सब लोग बहुत कुछ सीखते हैं
यह thread ऐसा लगता है जैसे math को अच्छी तरह लिखने के बारे में है
मैंने दशकों तक math पढ़ी, लिखी, पढ़ाई, apply की और publish की है, और applied mathematics में PhD भी ली है
math writing में समस्या है, यह सही है, और कुछ math बहुत खराब तरीके से लिखी जाती है
लेकिन काफ़ी अच्छी तरह लिखी गई math भी है
कम से कम हर symbol को इस्तेमाल से पहले define करना चाहिए, math पेश करने से पहले motivation देना मददगार होता है, और कभी-कभी intuitive explanation भी उपयोगी होती है
अच्छी तरह लिखी गई math को ध्यान से पढ़ना math writing सीखने में मदद करता है
उदाहरण के तौर पर Paul R. Halmos की Finite-Dimensional Vector Spaces, R. Creighton Buck की Advanced Calculus, Tom M. Apostol की Mathematical Analysis, H. L. Royden की Real Analysis, Walter Rudin की Real and Complex Analysis, Leo Breiman की Probability, Jacques Neveu की Mathematical Foundations of the Calculus of Probability को लिया जा सकता है
लेखक ने literature में विकसित तरीके के अनुसार ही Fermat’s Last Theorem को verify करने की कोशिश की, और इस प्रक्रिया में पाया कि एक subfield को सहारा देने वाला lemma जिस रूप में इस्तेमाल किया गया था, उस रूप में true नहीं है
फिर भी वह मानता है कि वह field कुल मिलाकर salvageable है, क्योंकि अगर वह सचमुच गलत होती तो किसी ने अब तक कोई negative result खोज लिया होता—इस भरोसे के कारण
अब उस field को सहारा देने के लिए suitable replacement ढूँढना था
लेखक काफ़ी मज़ेदार ढंग से लिखता है, इसलिए आधा भी समझ नहीं आया फिर भी पढ़ना आसान था—यह अजीब अनुभव था
जब कोई proof refute हो जाए या उसमें flaw मिल जाए, तो उसके लिए अच्छा शब्द vitiated मिला
मुझे यह इसलिए पसंद है कि इससे यह गलतफहमी कम होती है कि conclusion false साबित हो गया है, फिर भी यह अर्थ आ जाता है कि वह proof damaged है और उसे नए proof या repair की ज़रूरत है