पाँचवें Busy Beaver के साथ शोधकर्ता गणना की सीमाओं के करीब पहुँचे
(quantamagazine.org)- दुनिया भर के 20 से अधिक लोगों की भागीदारी वाले Busy Beaver Challenge ने 5-नियम Turing machine के Busy Beaver नंबर BB(5)=47,176,870 को सत्यापित किया
- 1989 में Marxen और Buntrock द्वारा खोजी गई मशीन, जो 47,176,870 steps के बाद रुकती है, वास्तव में सबसे लंबे समय तक चलने वाली 5-नियम रुकने वाली मशीन है, यह पुष्टि हो गई
- टीम ने duplicate candidates घटाने वाली वंशावली विधि, non-halting पहचानने वाले programs, और Coq proof assistant को मिलाकर करोड़ों candidates को process किया
- अंतिम परिणाम mxdys द्वारा community की techniques को एकीकृत कर बनाए गए 40,000-line Coq proof के रूप में पूरा हुआ, और Inria के Coq expert Yannick Forster ने इसकी समीक्षा की
- BB(6) में Collatz conjecture जैसी 6-नियम मशीन Antihydra एक बाधा बनकर सामने आई है, इसलिए BB(5) संभवतः वह अंतिम Busy Beaver number हो सकता है जिसे मानवता ठीक-ठीक जान पाएगी
BB(5) की पुष्टि हुई
- Busy Beaver Challenge टीम ने BB(5) के सटीक मान 47,176,870 को सत्यापित किया
- यह मान 5 नियमों वाली Turing machines में से रुकने वाली किसी मशीन द्वारा चलाए जा सकने वाले अधिकतम steps की संख्या बताता है
- सत्यापन में Coq proof assistant का उपयोग हुआ, और Coq प्रमाणित करता है कि mathematical proof बिना errors के बना है या नहीं
- Santa Fe Institute के Cristopher Moore ने इस काम की social और mathematical engineering को प्रभावशाली बताया
- Maynooth University के Damien Woods ने परिणाम आने की गति की तुलना “Usain Bolt territory” से की
- BB(5) का विशिष्ट मान दूसरे computer science क्षेत्रों में applications से अधिक, computability की सीमा पर मिली उपलब्धि होने के कारण अहम है
Busy Beaver समस्या और halting problem
- Busy Beaver समस्या सामान्य programming languages के बजाय Turing machines को लक्ष्य बनाती है
- Turing machine अनंत tape पर 0 और 1 को पढ़ती और लिखती है, और head एक-एक cell चलता हुआ rule table के अनुसार काम करता है
- हर rule, अभी पढ़े गए value के 0 या 1 होने के आधार पर अगली action तय करता है
- value बदलना या बनाए रखना
- बाएँ या दाएँ जाना
- अगला संदर्भित किया जाने वाला rule तय करना
- special rule तय करता है कि मशीन कब रुकेगी
- कोई Turing machine अंततः रुकेगी या हमेशा चलती रहेगी, इसे सामान्य रूप से तय करने की समस्या halting problem है
- Alan Turing ने साबित किया कि halting problem का कोई general solution नहीं है
- Busy Beaver की खोज, सभी machines के रुकने या न रुकने को सामान्य रूप से हल करने के बजाय, निश्चित नियम-संख्या वाले finite set में प्रत्येक मशीन को classify करने का काम है
Radó का Busy Beaver game
- Tibor Radó ने 1962 के paper में Turing machines को नियमों की संख्या के आधार पर समूहित कर Busy Beaver game परिभाषित किया
- n नियमों वाली सभी Turing machines के set में:
- कुछ machines हमेशा चलती रहती हैं
- कुछ machines रुकती हैं
- रुकने वाली machines में जो सबसे लंबे समय तक चलती है, वही busy beaver है
- उसके execution steps की संख्या BB(n) है
- BB(n) तय करने के लिए रुकने वाली सभी machines का running time जांचना और बाकी सभी machines के न रुकने को साबित करना होता है
- execution time मापना आम तौर पर computer simulation से संभव है, लेकिन non-halting proof किसी विशेष machine के लिए halting problem हल करने जैसा है
- Busy Beaver Challenge contributor Shawn Ligocki इस काम को “unknown की boundary” पर किया जाने वाला काम मानते हैं
BB(1) से BB(4) तक
- BB(1)=1 आसानी से verify हो जाता है
- यदि पहला rule 0 पढ़ने पर रुकने के लिए बनाया जाए, तो यह पहले step में रुकता है
- अन्यथा यह 0 से भरी tape के साथ आगे चलता रहता है
- सिर्फ 2 rules होने पर भी 6,000 से अधिक अलग-अलग Turing machines बनती हैं, 3 rules पर लाखों, और 4 rules पर अरबों तक संख्या बढ़ जाती है
- Allen Brady ने शुरुआती behavior समान रखने वाली machines को group कर duplicates घटाने वाली वंशावली विधि को computer program में integrate किया
- Shen Lin ने Radó के साथ BB(3)=21 साबित किया, और परिणाम 1965 में प्रकाशित हुआ
- Brady ने 1966 में 107 steps के बाद रुकने वाली 4-rule machine खोजी, और 1974 में साबित किया कि वही BB(4) है
- BB(4) इसके बाद 40 साल से अधिक समय तक मानवता को ज्ञात अंतिम Busy Beaver number था
पाँचवें Busy Beaver की खोज
- 1984 की Dortmund competition BB(5) की दिशा में पहला बड़े पैमाने का hunt था
- 5-rule Turing machines लगभग 17 trillion तक पहुँचती हैं, और यदि उन्हें प्रति millisecond एक के हिसाब से सूचीबद्ध करें तो भी 500 साल से अधिक लगेंगे
- Dortmund participants द्वारा पाई गई सबसे व्यस्त machine 100,000 से अधिक steps चलने के बाद रुकी
- बाद में एक researcher ने 20 लाख से अधिक steps चलने वाली machine खोजी
- Heiner Marxen और Jürgen Buntrock ने Turing machine simulation को तेज करने वाली mathematical techniques विकसित कीं
- Marxen ने 1989 में अपनी company के शक्तिशाली नए computer पर weekend भर program चलाया, और 47,176,870 steps के बाद रुकने वाली machine खोजी
- Buntrock ने परिणाम reproduce किया, और दोनों ने 1990 की शुरुआत में paper प्रकाशित किया
- वास्तव में यही machine पाँचवाँ Busy Beaver थी, लेकिन बाकी सभी machines के न रुकने को साबित करने में 30 साल से अधिक और लगे
Skelet और अनसुलझी machines
- 2000 के दशक की शुरुआत में Bulgarian computer scientist Georgi Ivanov Georgiev BB(5) के बेहद करीब पहुँच गए
- Georgiev ने 2 साल तक हर दिन कई घंटे non-halting machines की पहचान करने वाले program को सुधारने में लगाए
- अंतिम program comments के बिना compact code की 6,000 lines का था, और चलने में 1 सप्ताह से अधिक लगा
- इस program ने लगभग 100 Turing machines को unresolved छोड़ा, और Georgiev ने manual analysis से इसे 43 तक घटाया
- Georgiev ने 2003 में Skelet नाम के pseudonym से परिणाम online पोस्ट किए
- ये 43 कठिन machines उनके pseudonym पर Skelet machines कहलाने लगीं
- Georgiev ने कहा कि दो वर्षों के intensive work के बाद वे इतने थक गए थे कि अब नए ideas नहीं निकाल पा रहे थे
Busy Beaver Challenge की collaborative structure
- Tristan Stérin ने 2022 में Busy Beaver Challenge शुरू किया
- project online collaboration के तरीके से चला और 20 से अधिक लोगों की international community में बढ़ा, जिसमें पारंपरिक academic credentials न रखने वाले कई contributors शामिल थे
- Stérin का मानना था कि BB(5) को finalize करने के लिए documented और reproducible proof चाहिए
- Georgiev का program बहुत advanced था, लेकिन दूसरे researchers के लिए review करना कठिन था
- Stérin ने existing approach के आधार पर काम बाँटा
- Brady की वंशावली विधि से duplicate machines हटाना
- 47,176,870 steps के भीतर रुकने वाली machines की पहचान करना
- हमेशा चलने वाली machines को उनके proof methods वाले independent programs से handle करना
- 2021 के अंत में लिखे गए पहले-stage program ने BB(5) निर्धारित करने के लिए पर्याप्त लगभग 120 million Turing machines की list बनाई
- उनमें से लगभग एक-चौथाई Marxen और Buntrock की machine से पहले रुक गईं, और 88 million review के लिए बचीं
- Stérin ने machine behavior को 0 और 1 के 2D grid में दिखाने वाला spacetime diagram online interface भी बनाया
closed tape language और collaboration की रफ्तार
- Shawn Ligocki 2022 में Busy Beaver Challenge से जुड़े और Marxen द्वारा बनाई गई closed tape language method को फिर से सक्रिय किया
- यह method Turing machine tape के patterns का उपयोग कर machine के न रुकने को दिखाने के लिए एक unified mathematical framework देता है
- Ligocki ने technique को introduce करने वाला blog post लिखा, लेकिन उन्हें नहीं पता था कि सभी cases को cover करने वाला program कैसे लिखा जाए
- Justin Blanchard ने project से जुड़ने के बाद इसे implement किया, और दो अन्य contributors ने execution speed को बहुत बढ़ाया
- कुछ महीनों में closed tape language method टीम के सबसे powerful tools में से एक बन गया
- यह technique Georgiev द्वारा छोड़ी गई 43 Skelet machines में से 10 को भी handle कर सकी
- Ligocki मानते हैं कि यह परिणाम किसी एक व्यक्ति के योगदान से संभव नहीं होता
Skelet #1, Skelet #17, और Coq
- Skelet #1 ऐसी machine थी जो predictable phases और chaotic phases को बारी-बारी दिखाती थी
- मार्च 2023 में Ligocki और Pavel Kropitz ने Marxen और Buntrock की 30 साल पुरानी accelerated simulation technique को मजबूत कर Skelet #1 का analysis किया
- Skelet #1 1 trillion×1 trillion steps से आगे जाने के बाद ही repeating cycle में गई, और वह repeating cycle 8 billion steps से अधिक लंबी थी
- 21 वर्षीय self-taught programmer mei ने Coq सीखने के बाद Busy Beaver Challenge के कई proofs को Coq में translate किया
- mei ने Ligocki और Kropitz के Skelet #1 non-halting proof को भी Coq में बदला, जिससे वह result अधिक भरोसेमंद बना
- Skelet #17 एक और कठिन machine थी, जिसमें Chris Xu ने breakthrough किया
- Xu का proof शानदार था, लेकिन उसमें ऐसी mathematical intuition शामिल थी जिसे Coq द्वारा मांगे गए precise formal format में बदलना कठिन था
- टीम “6 महीने तक program चलाओ” जैसे proof के बजाय reasonable तरीके से reproducible proof चाहती थी
40,000-line Coq proof
- अप्रैल 2024 में mxdys नामक pseudonym से जाने जाने वाले नए contributor Coq proof पूरा करने के काम में जुड़े
- mxdys की location या personal background टीम को भी नहीं पता
- 10 मई को mxdys ने Discord पर “The Coq proof of BB(5) is finished.” पोस्ट किया
- mxdys ने कुछ हफ्तों में community की techniques और results को integrate कर single 40,000-line Coq proof पूरा किया
- proof Coq-BB5 repository में public किया गया
- Inria के Coq expert Yannick Forster ने इस proof की review की, और कहा कि इसे formalize करना आसान काम नहीं था
- परिणामस्वरूप Marxen और Buntrock द्वारा 30 साल से अधिक पहले खोजी गई 47,176,870-step machine वास्तव में पाँचवाँ Busy Beaver है, यह पक्का हो गया
- Georgiev ने बताया कि उन्हें उम्मीद नहीं थी कि यह समस्या उनके जीवनकाल में हल हो जाएगी
- Allen Brady proof पूरा होने से एक महीने पहले, 21 अप्रैल 2024 को 90 वर्ष की उम्र में निधन हो गया
BB(6) और अगली सीमा
- Busy Beaver Challenge contributors ने परिणाम समझाने वाला formal academic paper तैयार करना शुरू किया
- paper में mxdys के Coq proof के साथ human-readable proof जोड़ा जाएगा
- टीम के कुछ सदस्य अगले Busy Beaver की ओर बढ़ गए
- mxdys और Racheline ने BB(6) में ऐसी बाधा खोजी जो पार करना मुश्किल लगती है
- यह बाधा Collatz conjecture जैसी halting problem वाली 6-rule machine है
- इस machine को Antihydra कहा जाता है
- Turing machines और Collatz conjecture का संबंध Pascal Michel के 1993 paper तक जाता है, लेकिन Antihydra ऐसी सबसे छोटी machine लगती है जिसे mathematics में conceptual breakthrough के बिना हल नहीं किया जा सकता
- Scott Aaronson मानते हैं कि BB(5) मानवता को ज्ञात होने वाला अंतिम Busy Beaver number हो सकता है
- कुछ contributors Busy Beaver के variant problems पर काम जारी रखने की योजना रखते हैं, लेकिन सभी participants उसी दिशा में नहीं रहेंगे
- Stérin Busy Beaver Challenge के जरिए online collaborative research methods की प्रभावशीलता को लेकर आश्वस्त हुए, और mathematics के अन्य क्षेत्रों में collaborative projects की मदद करने वाले software tools विकसित करना चाहते हैं
1 टिप्पणियां
Hacker News टिप्पणियाँ
Scott Aaronson ने इस परिणाम पर एक टिप्पणी लिखी है: https://scottaaronson.blog/?p=8088
और “leisure-class beavers” के बारे में इस साल की शुरुआत के बड़े threads भी हैं:
https://news.ycombinator.com/item?id=40453221
https://news.ycombinator.com/item?id=38113792
https://news.ycombinator.com/item?id=37910297
मूल Busy Beaver समस्या के कई variants हैं, जिनमें से एक lambda calculus से define किया गया functional Busy Beaver है [1]
इसमें states की संख्या के बजाय bit-level program size मापा जाता है, इसलिए ज्यादा values निर्धारित की जा सकती हैं; अब तक Turing machines के लिए सिर्फ 6 तक है, जबकि इस तरफ 37 तक निकल चुका है। ज्ञात maximum और Graham's Number से आगे की value के बीच का अंतर भी केवल 13 program bits का है। एक निकट variant [2] को सीधे Kolmogorov complexity से व्यक्त किया जा सकता है, और Mikhail Andreev [3] information theory applications के लिए इसे महत्वपूर्ण मानते हैं
[1] https://oeis.org/A333479
[2] https://oeis.org/A361211
[3] https://arxiv.org/pdf/1703.05170
https://oeis.org/A141475 मिला, पर यहाँ 5 के लिए 27 trillion बताया गया है
मुझे याद है कि मैंने उस definition को समझाने वाला एक video देखा था
मैंने कुछ सालों तक एक ऐसे engineer के साथ काम किया था, जो elite tech company में मेरे देखे किसी भी व्यक्ति से तेज़ी से IC ranks में ऊपर गया था—बेहद और समझ से परे smart
वह कुछ साल पहले चला गया, और जब मैंने उससे plans पूछे तो उसने कहा कि वह Busy Beaver problem पर research करेगा। article में BB(5) की formal proof पूरी करने वाले anonymous contributor mxdys वही व्यक्ति हैं या नहीं, यह सोचता हूँ, लेकिन शायद कभी पता नहीं चलेगा
reward क्या है, यह समझ नहीं आता; और इतनी brilliant बुद्धि हो तो काश वह दुनिया को बेहतर बनाने से ज्यादा जुड़े problems हल करे
Tibor Radó का मूल Busy Beaver paper “On Non-Computable Functions” असल में काफी आसान और रोचक पढ़ाई है
अतिरिक्त annotations वाला modern version यहाँ है: https://data.jigsaw.nl/Rado_1962_OnNonComputableFunctions_Re...
यहाँ जो बात ध्यान खींचती है, वह यह है कि proof एक Coq proof है
यह जानना चाहूँगा कि क्या यह किसी पहले से ज्ञात proof को theorem prover में port करने के बजाय, शुरू से theorem prover में implemented कोई पहली महत्वपूर्ण proof है। पहले भी computer-assisted proofs थीं, लेकिन 4-color theorem या Kepler conjecture को formal verification environment में बाद में ही ले जाया गया था
मुख्य समस्या यह थी कि deciders और हाथ से किए गए proofs व्यवस्थित नहीं थे और कुछ हद तक संदिग्ध थे। खासकर Skelet #1 को final pattern तक accelerate करने के लिए dedicated program चाहिए था [0], और Skelet #17 के लिए Xu को non-halting prove करने में 7 पन्नों की dense reasoning लिखनी पड़ी थी [1]. पूरी Coq proof इन results को जरूरी भरोसा देती है
[0] https://www.sligocki.com/2023/03/13/skelet-1-infinite.html
[1] https://discuss.bbchallenge.org/t/skelet-17-does-not-halt/18...
https://github.com/ccz181078/Coq-BB5/blob/main/BB52Theorem.v
https://en.m.wikipedia.org/wiki/Four_color_theorem
हो सकता है मैंने “formal verification environment” का सही मतलब नहीं समझा हो, लेकिन मेरी जानकारी में 4-color theorem शुरुआत से ही computer से prove की गई थी। Kempe की original proof attempt में flaw था, लेकिन उसने बाद की proofs में इस्तेमाल हुए कुछ basic tools दिए, और आखिरकार theorem computer से prove हुई लगती है
यह Busy Beaver 1990 में खोजा गया था, और size 5 की सभी machines भी शायद उसके तुरंत बाद enumerate कर दी गई होंगी
टीम को बधाई। अब खाली tape के आधार पर 5-state 2-symbol Turing machine प्रोग्रामों की halting problem हल हो गई मानी जा सकती है
उत्सुकता है कि क्या किसी ने यही तकनीक 2-state 4-symbol वाले मामले पर लागू करके देखी है। आम तौर पर symbols, states से ज्यादा शक्तिशाली होते हैं, लेकिन वह स्तर शायद संभाला जा सकता है और कुछ अप्रत्याशित नतीजे भी मिल सकते हैं। 6-state 2-symbol और 2-state 5-symbol दोनों ही कठिन लगते हैं, और शायद सिद्ध रूप से कठिन भी हो सकते हैं। साथ ही, यह बेतुका लेकिन अजीब तरह से व्यापक विचार है कि इंसान मन की आंख या दिमाग के भीतर quantum mechanics जैसी किसी चीज़ से halting problem के जवाब intuit कर सकते हैं; जाहिर है, इस proof में ऐसी कोई चीज़ शामिल नहीं थी
जहां तक मुझे पता है, अभी इस्तेमाल हो रहे deciders ही 2×4 के बाकी सभी cases को non-halting साबित करने के लिए पर्याप्त हैं। इसलिए अगर decider design में कोई बड़ी गलती नहीं है, तो मौजूदा champion से Σ(2,4) = 2,050, S(2,4) = 3,932,964 निकलता है। बस नतीजे एक जगह संकलित नहीं किए गए हैं
2×5 में Hydra है और 6×2 में Antihydra है; दोनों केवल starting point और halt condition में अलग हैं, बाकी वही iteration compute करते हैं। standard conjecture यह है कि Mahler के 3/2 problem से जुड़ा यह iteration mod 2 में equidistributed है, और उस conjecture को सिद्ध करने पर 0 और 1 के cumulative ratio के upper और lower bounds मिलेंगे, जिससे दोनों machines के non-halting को लगभग निश्चित रूप से साबित किया जा सकेगा। बेशक, कोई ज्ञात proof method नहीं है
उन्होंने Aleph* नाम की logic theory-आधारित proof generator का इस्तेमाल किया, और तब तक 1,500 साल पहले से ही यह ज्ञात था कि ZFC, BB(18) को स्थापित नहीं कर सकता। 2024 से तुलना करें तो Aleph* के इस्तेमाल से बहुत पहले का कोई भी program, theory में भी, BB(18) हल करने के लिए brute-force proof checking में इस्तेमाल नहीं किया जा सकता था। यह आज हमारे ZFC proofs को enumerate और check करके theory में BB(??) हल कर सकने से अलग है
“इंसान halting problem के जवाब intuit करते हैं” वाला रुख इसी अर्थ में है। जहां तक मुझे पता है, ऐसी future history असंभव है, इसका कोई मजबूत theoretical कारण नहीं है। और Busy Beaver uncomputable है, इसलिए जरूरी program बनाने के लिए इंसानों को नई theory विकसित करनी पड़ी होगी। नतीजे का श्रेय किसी चीज़ को मिलना चाहिए, और उस समय program मौजूद नहीं था, इसलिए इसे computation को नहीं दिया जा सकता
उत्सुकता है कि लंबाई 5 के सभी non-halting programs संयोग से सभी non-halting साबित करने योग्य ही थे या नहीं
“यह fact कि Σ(5) = 1,915 और S(5) = 2,358,064 है, कभी साबित नहीं होगा। या अगर कोई और बड़ा lower bound मिल जाए, तो इस prediction में वह नया value लगा दें।”
वजह यह थी कि संभावना अधिक थी कि nature ने 5-state holdout machines के बीच Goldbach conjecture जितनी ही elusive कम-से-कम एक problem रख दी हो। दूसरे शब्दों में, हमारी पहचानने की क्षमता से परे कोई non-halting recursive pattern होने की संभावना अधिक थी। सौभाग्य से यह prediction सच नहीं हुआ, लेकिन फर्क बस एक extra state का था
[0] Allen Brady, "The Busy Beaver Game and the Meaning of Life", in Rolf Herken (ed.), The Universal Turing Machine: A Half-Century Survey, Oxford University Press, 1988, pp. 259–277. This chapter can also be found in the 2nd ed., Springer, 1995, pp. 237–254.
practical sense में तो दूसरे लोग पहले ही जवाब दे चुके हैं। mathematical sense में, अगर BB(5) undecidable होता तो काफी हैरानी होती। क्योंकि 5-state 2-symbol, undecidable behavior encode करने के लिए बहुत छोटा है
हालांकि incompleteness theorem के नतीजे के रूप में, कोई n जरूर मौजूद है जिसके लिए standard mathematics BB(n) का value साबित नहीं कर सकता। हाल के वर्षों में कई लोगों ने ऐसा n खोजकर उसे कितना कम किया जा सकता है, इस पर काम किया है, और वर्तमान record[0] 745 है। यह record शायद और कम किया जा सकता है, लेकिन फिर भी हमारे ज्ञात सबसे ऊंचे value 5 और जिसके अज्ञात होने का हमें पता है उस सबसे निचले value 745 के बीच बड़ा फासला है
[0] “standard mathematics” क्या है, अगर यह जानना चाहें तो जोड़ दूं कि यह ZFC और PA दोनों के लिए मौजूदा record है। इसलिए कम-से-कम PA के लिए इसे और कम करना संभव होना चाहिए लगता है। अब तक शायद PA में ZFC से बेहतर तरीका नहीं मिला है, लेकिन स्वाभाविक रूप से संभव होना चाहिए, है न?
“सिर्फ चार दिन पहले, mxdys और Racheline नाम के एक और contributor ने BB(6) के लिए ऐसी बाधा खोजी जो पार करना मुश्किल लगती है। यह 6-rule machine है जिसकी halting problem, मशहूर तौर पर कठिन mathematical problem Collatz conjecture जैसी दिखती है। Turing machines और Collatz conjecture का संबंध mathematician Pascal Michel के 1993 के paper तक जाता है, लेकिन नई खोजी गई ‘Antihydra’ नाम की machine ऐसी सबसे छोटी machine लगती है जिसे mathematics में conceptual breakthrough के बिना हल नहीं किया जा सकता।”
एक personal project में मैंने cutting stock problem(https://en.wikipedia.org/wiki/Cutting_stock_problem) हल करने वाला program लिखा था
stock में /---/, /---|, |---| आकार के piece cuts शामिल थे और मैं 45-degree cuts में material waste नहीं करना चाहता था, इसलिए existing programs का इस्तेमाल नहीं कर सकता था या करना नहीं चाहता था। Brady ने BB(4) search को optimize करने के लिए उन search subtrees को काटा जहां differences मायने नहीं रखते थे—यह बात मेरे program को तेज बनाते समय मैंने जो किया था उससे काफी मिलती-जुलती लगी, इसलिए दिलचस्प है
Scott Aaronson के blog post के अनुसार 5-state Turing machines 16,679,880,978,201 हैं
उत्सुकता है कि इनमें से कितने percent halt करते हैं। Edit: n-state Turing machines की संख्या (4n + 1)^(2n) है। छोटे n के लिए वैसी ही analysis जैसी मैं जानना चाहता था, उसका data मिला: https://github.com/LukasKalbertodt/beaver
bbchallenge.org site पर नहीं मिला, लेकिन सभी machines classified हैं
कुल मिलाकर, proof काफ़ी छोटा है। spaces और comments सहित यह Coq की 19,000 lines है
मेरे अनुभव में, अगर इसे पारंपरिक paper में compile किया जाए, तो यह Coq version से काफ़ी छोटा हो जाएगा। बेशक proof की लंबाई difficulty या complexity का पैमाना नहीं है, लेकिन बहुत मोटे तौर पर इसे एक संकेतक की तरह इस्तेमाल किया जा सकता है
जब मानव ज्ञान की सीमाओं की बात होती है, तो अक्सर ऐसे प्रमेय याद आते हैं जिन्हें prove तो किया जा सकता है, लेकिन जो इतने जटिल हैं कि कोई भी इंसान उन्हें समझ नहीं सकता। शायद हमारे पास मौजूद सबसे जटिल proof finite simple groups का classification है; यह हजारों-लाखों pages में फैला है और संभव है कि पृथ्वी पर बहुत कम, या शायद कोई भी, इसे पूरी तरह समझता न हो
article में कहा गया है कि BB(6) undecidable हो सकता है। लेकिन यह भी संभव है कि इसका proof लाखों pages का हो और इसलिए मानवता की पहुंच से बाहर हो