Lean4 ने Terence Tao के हालिया पेपर में एक छोटी बग खोजने में मदद की

 (mathstodon.xyz)
3 पॉइंट द्वारा GN⁺ 2023-10-28 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • Terence Tao की mathstodon.xyz पोस्ट
  • Terence Tao के हालिया पेपर में Lean4 formalization project की वजह से एक छोटी लेकिन महत्वपूर्ण बग मिली
  • पेपर के पेज 6 को formalize करने की प्रक्रिया में बग मिली; पेपर https://arxiv.org/pdf/2310.05328.pdf पर देखा जा सकता है
  • Tao के पेपर में n=3, k=2 के मामले में divergence देने वाला expression 12log⁡n−1n−k−1 मिला
  • समस्या सिर्फ n के छोटे मानों में मौजूद है और पेज पर कुछ numerical constants बदलकर इसे ठीक किया जा सकता है
  • n≥8 के लिए logic अब भी वैध है, और छोटे n के मामले को अधिक सरल तरीके से संभाला जा सकता है
  • Lean4 ने Tao से 0<n−3 सिद्ध करने को कहा, लेकिन उनके पास सिर्फ n>2 की hypothesis थी, जिससे विरोधाभास सामने आया
  • Tao ने Lean4 में formalization आज़माने के बाद मिली इस छोटी त्रुटि को स्वीकार करने वाला एक footnote पेपर के नए संस्करण में जोड़ने की योजना बनाई है
  • इस पोस्ट ने समुदाय की रुचि और सकारात्मक प्रतिक्रिया पैदा की, और भविष्य के काम के लिए मज़बूत आधार स्थापित करने में proof assistants के महत्व को रेखांकित किया

संबंधित पढ़ाई

1 टिप्पणियां

 
GN⁺ 2023-10-28
Hacker News की राय
  • प्रसिद्ध गणितज्ञ टेरेंस टाओ ने Lean4 और GPT4 का उपयोग करके अपने हालिया शोधपत्र में एक छोटा बग खोजा।
  • Lean4 सीखने की टाओ की प्रक्रिया उनके Mastodon पोस्टों में दर्ज है, जिससे यह इस बात का एक दिलचस्प केस स्टडी बनता है कि Lean4 काम को कैसे तेज़ कर सकता है।
  • शुरुआती लोगों के लिए Natural Number Game को Lean4 के आसान परिचय के रूप में सुझाया गया है।
  • एक उपयोगकर्ता ने Lamport के TLA+ का उपयोग करके formal specifications बनाने और प्रोग्रामिंग में गलतियाँ कम करने का अपना अनुभव साझा किया।
  • कंपाइलर में इसे लागू करने की जटिलता के बावजूद, dependent types को लेकर रुचि बनी हुई है।
  • Lean4 और automated theorem proving का संयोजन भविष्य के लिए एक आशाजनक तकनीकी मेल लगता है, जो नई खोजों को बढ़ावा दे सकता है।
  • टाओ द्वारा Copilot का उपयोग करके Lean सीखना इस बात के उदाहरण के रूप में रेखांकित किया गया कि Lean4 नए टूल अपनाने में होने वाली रुकावट को कैसे कम कर सकता है।
  • Lean4 पर टाओ की प्रगति उनके GitHub पर देखी जा सकती है।
  • एक उपयोगकर्ता ने formal proof checkers और language models को जोड़कर synthetic conjecture-proof pairs बनाने का विचार सुझाया, जो proof generation में अतिमानवीय क्षमता तक बढ़ सकता है।
  • "बग" शब्द का उपयोग गणितीय त्रुटि का वर्णन करने के लिए किया गया, जिसे कुछ उपयोगकर्ताओं ने असामान्य माना।