Araştırmacılar Beşinci Busy Beaver ile Hesaplamanın Sınırına Yaklaştı
(quantamagazine.org)- Dünya genelinden 20’den fazla kişinin katıldığı Busy Beaver Challenge, 5 kurallı Turing makinesinin Busy Beaver sayısı olan BB(5)=47.176.870 değerini doğruladı
- Marxen ve Buntrock’ın 1989’da bulduğu, 47.176.870 adım sonra duran makinenin gerçekten en uzun çalışan 5 kurallı duran makine olduğu kesinleşti
- Ekip; yinelenen adayları azaltan soy ağacı yöntemi, durmama belirleme programları ve Coq proof assistant’ı birleştirerek on milyonlarca adayı işledi
- Nihai sonuç, mxdys’in topluluğun tekniklerini birleştirdiği 40.000 satırlık Coq kanıtı ile tamamlandı ve Inria’dan Coq uzmanı Yannick Forster tarafından incelendi
- BB(6)’da, Collatz conjecture’a benzeyen 6 kurallı makine Antihydra bir engel olarak ortaya çıkıyor; bu yüzden BB(5), insanlığın kesin olarak bileceği son Busy Beaver sayısı olabilir
BB(5) kesinleşti
- Busy Beaver Challenge ekibi BB(5)’in kesin değerini 47.176.870 olarak doğruladı
- Bu değer, 5 kurala sahip Turing makineleri arasında duran bir makinenin çalışabileceği en yüksek adım sayısını ifade ediyor
- Doğrulamada Coq proof assistant kullanıldı; Coq, matematiksel kanıtın hatasız biçimde oluşturulup oluşturulmadığını onaylıyor
- Santa Fe Institute’tan Cristopher Moore, bu çalışmanın sosyal ve matematiksel mühendisliğini etkileyici bulduğunu söyledi
- Maynooth University’den Damien Woods, sonucun ortaya çıkma hızını “Usain Bolt territory” benzetmesiyle anlattı
- BB(5)’in somut değerinde asıl önemli nokta, diğer bilgisayar bilimi alanlarındaki uygulamalardan ziyade hesaplanamazlığın sınırında elde edilmiş bir başarı olması
Busy Beaver problemi ve durma problemi
- Busy Beaver problemi genel programlama dillerini değil, Turing makinelerini konu alır
- Turing makinesi, sonsuz bir şerit üzerindeki 0 ve 1’leri okur ve yazar; head her seferinde bir hücre hareket ederek kural tablosuna göre çalışır
- Her kural, o anda okunan değerin 0 mı 1 mi olduğuna göre bir sonraki eylemi belirler
- Değeri değiştirir ya da aynı bırakır
- Sola veya sağa hareket eder
- Sonraki başvurulacak kuralı belirler
- Özel bir kural, makinenin ne zaman duracağını belirler
- Bir Turing makinesinin sonunda durup durmayacağını ya da sonsuza dek çalışıp çalışmayacağını genel olarak belirleme problemi durma problemidir
- Alan Turing, durma probleminin genel bir çözümü olmadığını kanıtladı
- Busy Beaver avı, tüm makinelerin durup durmadığını genel olarak çözmek yerine, kural sayısı sabit olan sonlu bir küme içinde her makineyi sınıflandırma işidir
Radó’nun Busy Beaver game’i
- Tibor Radó, 1962 tarihli makalesinde Turing makinelerini kural sayılarına göre gruplayarak Busy Beaver game’i tanımladı
- Kural sayısı n olan tüm Turing makineleri kümesinde:
- Bazı makineler sonsuza dek çalışır
- Bazı makineler durur
- Duran makineler içinde en uzun çalışan makine busy beaver’dır
- Bu çalışmanın adım sayısı BB(n)’dir
- BB(n)’i kesinleştirmek için duran tüm makinelerin çalışma sürelerini kontrol etmek ve geri kalan tüm makinelerin durmadığını kanıtlamak gerekir
- Çalışma süresini ölçmek genellikle bilgisayar simülasyonuyla mümkündür; ancak durmama kanıtı, belirli bir makine için durma problemini çözmeye yakındır
- Busy Beaver Challenge katkıcılarından Shawn Ligocki, bu çalışmayı “bilinmeyenin sınırında” yürütülen bir iş olarak görüyor
BB(1)’den BB(4)’e
- BB(1)=1 kolayca doğrulanır
- İlk kural, 0 okuduğunda duracak şekilde ayarlanırsa ilk adımda durur
- Diğer durumlarda 0’larla dolu şerit boyunca hareket etmeyi sürdürür
- Yalnızca 2 kural olduğunda bile 6.000’den fazla farklı Turing makinesi ortaya çıkar; 3 kuralda milyonlara, 4 kuralda milyarlara yükselir
- Allen Brady, ilk davranışları aynı olan makineleri gruplayarak tekrarları azaltan soy ağacı yöntemini bir bilgisayar programına entegre etti
- Shen Lin, Radó ile birlikte BB(3)=21 olduğunu kanıtladı ve sonuç 1965’te yayımlandı
- Brady, 1966’da 107 adım sonra duran 4 kurallı bir makine keşfetti; 1974’te de bunun BB(4) olduğunu kanıtladı
- BB(4), sonraki 40 yılı aşkın süre boyunca insanlığın bildiği son Busy Beaver sayısıydı
Beşinci Busy Beaver avı
- 1984’te Dortmund yarışması, BB(5) için ilk büyük ölçekli avdı
- 5 kurallı Turing makinelerinin sayısı neredeyse 17 trilyona ulaşır; milisaniyede bir tane listelense bile 500 yıldan fazla sürer
- Dortmund katılımcılarının bulduğu en çalışkan makine, 100.000’den fazla adım çalıştıktan sonra duruyordu
- Daha sonra bir araştırmacı, 2 milyondan fazla adım çalışan bir makine buldu
- Heiner Marxen ve Jürgen Buntrock, Turing makinesi simülasyonunu hızlandıran matematiksel teknikler geliştirdi
- Marxen, 1989’da şirketinin güçlü yeni bilgisayarında programı hafta sonu boyunca çalıştırdı ve 47.176.870 adım sonra duran bir makine buldu
- Buntrock sonucu yeniden üretti ve ikisi 1990 başında bir makale yayımladı
- Aslında bu makine beşinci Busy Beaver’dı; ancak kalan tüm makinelerin durmadığını kanıtlamak için 30 yıldan fazla daha gerekti
Skelet ve çözülemeyen makineler
- 2000’lerin başında Bulgar bilgisayar bilimci Georgi Ivanov Georgiev, BB(5)’e çok yaklaştı
- Georgiev, durmayan makineleri tanımlayan programını geliştirmek için 2 yıl boyunca her gün saatler harcadı
- Nihai program, yorum satırı içermeyen yoğun 6.000 satırlık koddan oluşuyordu ve çalışması 1 haftadan uzun sürdü
- Bu program yaklaşık 100 Turing makinesini çözümsüz bıraktı; Georgiev elle analizle bunu 43’e indirdi
- Georgiev, 2003’te sonuçlarını Skelet takma adıyla çevrimiçi yayımladı
- Bu 43 zor makine, onun takma adına atıfla Skelet machines olarak anılmaya başladı
- Georgiev, iki yıllık yoğun çalışmanın ardından artık yeni fikir üretemeyecek kadar tükendiğini söyledi
Busy Beaver Challenge’ın iş birliği yapısı
- Tristan Stérin, 2022’de Busy Beaver Challenge’ı başlattı
- Proje çevrimiçi iş birliğiyle yürütüldü ve geleneksel akademik unvanlara sahip olmayan çok sayıda katkıcının da yer aldığı, 20’den fazla kişilik uluslararası bir topluluğa dönüştü
- Stérin, BB(5)’i kesinleştirmek için belgelenmiş ve yeniden üretilebilir bir kanıt gerektiğini düşünüyordu
- Georgiev’in programı çok gelişmişti, ancak diğer araştırmacıların incelemesi zordu
- Stérin, mevcut yaklaşımlara dayanarak işi parçalara böldü
- Brady’nin soy ağacı yöntemiyle yinelenen makineleri eledi
- 47.176.870 adım içinde duran makineleri belirledi
- Sonsuza dek çalışan makineleri, her bir kanıt yöntemini içeren bağımsız programlarla ele aldı
- 2021 sonlarında yazılan ilk aşama programı, BB(5)’i belirlemek için yeterli olan yaklaşık 120 milyon Turing makinesi listesi üretti
- Bunların yaklaşık dörtte biri Marxen ve Buntrock’ın makinesinden önce durdu; 88 milyon makine inceleme adayı olarak kaldı
- Stérin ayrıca makine davranışını 0 ve 1’lerden oluşan iki boyutlu bir ızgara olarak gösteren uzay-zaman diyagramı çevrimiçi arayüzü de kurdu
Kapalı şerit dili ve iş birliğinin hızlanması
- Shawn Ligocki, 2022’de Busy Beaver Challenge’a katılarak Marxen’in geliştirdiği kapalı şerit dili yöntemini yeniden canlandırdı
- Bu yöntem, Turing makinesi şeridindeki örüntüleri kullanarak makinenin durmadığını göstermeye yönelik birleşik bir matematiksel çerçeve sağlar
- Ligocki, tekniği tanıtan bir blog yazısı yazdı; ancak tüm durumları kapsayacak bir programın nasıl yazılacağını bilmiyordu
- Justin Blanchard projeye katıldıktan sonra bunu uyguladı; iki başka katkıcı da çalışma hızını büyük ölçüde artırdı
- Birkaç ay içinde kapalı şerit dili yöntemi ekibin en güçlü araçlarından biri oldu
- Bu teknik, Georgiev’in geride bıraktığı 43 Skelet machine’dan 10’unu da ele alabildi
- Ligocki, bu sonucun tek bir kişinin katkısıyla ortaya çıkmış olmayacağını düşünüyor
Skelet #1, Skelet #17 ve Coq
- Skelet #1, öngörülebilir aşamalar ile kaotik aşamaları dönüşümlü olarak gösteren bir makineydi
- Mart 2023’te Ligocki ve Pavel Kropitz, Marxen ve Buntrock’ın 30 yıllık hızlandırılmış simülasyon tekniğini güçlendirerek Skelet #1’i analiz etti
- Skelet #1 ancak 1 trilyon×1 trilyon adımı aştıktan sonra tekrar döngüsüne girdi ve bu tekrar döngüsü 8 milyardan fazla adım uzunluğundaydı
- 21 yaşındaki kendi kendini yetiştirmiş programcı mei, Coq’yu öğrendikten sonra Busy Beaver Challenge’ın çeşitli kanıtlarını Coq’ya çevirdi
- mei, Ligocki ve Kropitz’in Skelet #1 durmama kanıtını da Coq’ya taşıyarak bu sonucu daha sağlam hale getirdi
- Skelet #17, Chris Xu’nun atılım yaptığı bir başka zor makineydi
- Xu’nun kanıtı etkileyiciydi; ancak Coq’nun gerektirdiği kesin biçimsel forma aktarılması zor matematiksel sezgiler içeriyordu
- Ekip, “programı 6 ay çalıştırın” tarzı bir kanıt değil, makul ölçüde yeniden üretilebilir bir kanıt istiyordu
40.000 satırlık Coq kanıtı
- Nisan 2024’te, yalnızca mxdys takma adıyla bilinen yeni bir katkıcı Coq kanıtını tamamlama çalışmasına katıldı
- mxdys’in konumunu ya da kişisel geçmişini ekip de bilmiyor
- 10 Mayıs’ta mxdys Discord’a “The Coq proof of BB(5) is finished.” diye yazdı
- mxdys, birkaç hafta içinde topluluğun tekniklerini ve sonuçlarını bir araya getirerek tek bir 40.000 satırlık Coq kanıtını tamamladı
- Kanıt Coq-BB5 deposunda yayımlandı
- Inria’dan Coq uzmanı Yannick Forster bu kanıtı inceledi ve biçimselleştirmenin kolay bir iş olmadığını belirtti
- Sonuç olarak Marxen ve Buntrock’ın 30 yılı aşkın süre önce bulduğu 47.176.870 adımlık makinenin gerçekten beşinci Busy Beaver olduğu kesinleşti
- Georgiev, bu problemin kendi yaşamı içinde çözüleceğini beklemediğini aktardı
- Allen Brady, kanıtın tamamlanmasından bir ay önce, 21 Nisan 2024’te 90 yaşında hayatını kaybetti
BB(6) ve bir sonraki sınır
- Busy Beaver Challenge katkıcıları, sonucu açıklayan resmi bir akademik makale hazırlamaya başladı
- Makale, mxdys’in Coq kanıtını insan tarafından okunabilir bir kanıtla tamamlayacak şekilde hazırlanacak
- Bazı ekip üyeleri bir sonraki Busy Beaver’a geçti
- mxdys ve Racheline, BB(6)’da aşılması zor görünen bir engel keşfetti
- Bu engel, Collatz conjecture’a benzeyen bir durma problemine sahip 6 kurallı bir makine
- Bu makine Antihydra olarak adlandırılıyor
- Turing makineleri ile Collatz conjecture arasındaki bağlantı Pascal Michel’in 1993 tarihli makalesine kadar uzanıyor; ancak Antihydra, matematikte kavramsal bir atılım olmadan çözülemeyecek gibi görünen en küçük makine
- Scott Aaronson, BB(5)’in insanlığın öğreneceği son Busy Beaver sayısı olabileceğini düşünüyor
- Bazı katkıcılar Busy Beaver’ın varyant problemleri üzerinde çalışmayı sürdürecek; ancak tüm katılımcılar aynı yönde kalmış değil
- Stérin, Busy Beaver Challenge sayesinde çevrimiçi iş birliğine dayalı araştırma yönteminin etkinliğine ikna oldu ve matematiğin başka alanlarındaki iş birliği projelerine yardımcı olacak yazılım araçları geliştirmek istiyor
1 yorum
Hacker News yorumları
Scott Aaronson’ın bu sonuç hakkında yazdığı bir yorum var: https://scottaaronson.blog/?p=8088
Ayrıca “leisure-class beavers” ile ilgili bu yılın başından büyük başlıklar da var:
https://news.ycombinator.com/item?id=40453221
https://news.ycombinator.com/item?id=38113792
https://news.ycombinator.com/item?id=37910297
Aslında Busy Beaver probleminin birçok varyasyonu var; bunlardan biri lambda hesabıyla tanımlanan işlevsel Busy Beaver [1]
Durum sayısı yerine bit cinsinden program boyutu ölçüldüğü için daha fazla değer belirlenebiliyor; şimdiye kadar Turing makineleri tarafında yalnızca 6 değer varken bu tarafta 37’ye kadar çıkılmış. Bilinen en büyük değer ile Graham's Number’ı aşan bir değer arasındaki fark da yalnızca 13 bitlik program. Yakından ilişkili bir varyasyon [2] Kolmogorov karmaşıklığıyla doğrudan ifade edilebiliyor ve Mikhail Andreev [3] bunun bilgi teorisi uygulamaları açısından önemli olduğunu düşünüyor
[1] https://oeis.org/A333479
[2] https://oeis.org/A361211
[3] https://arxiv.org/pdf/1703.05170
https://oeis.org/A141475 adresini buldum ama burada 5 için 27 trilyon deniyor
Bu tanımı açıklayan bir video izlediğimi hatırlıyorum
Seçkin bir teknoloji şirketinde, gördüğüm herkesten daha hızlı IC seviyelerinde yükselen, olağanüstü ve anlaşılması zor ölçüde zeki bir mühendisle birkaç yıl çalıştım
Birkaç yıl önce ayrıldı; planını sorduğumda Busy Beaver problemi üzerinde çalışacağını söyledi. Makalede BB(5)’in biçimsel ispatını tamamlayan anonim katkıcı mxdys acaba o kişi mi diye merak ediyorum ama muhtemelen bunu hiçbir zaman öğrenemeyeceğim
Ödülün ne olduğunu bilmiyorum; böyle parlak bir zekânın dünyayı iyileştirmeyle daha ilgili bir problemi çözmesini isterdim
Tibor Radó’nun orijinal Busy Beaver makalesi “On Non-Computable Functions” aslında oldukça kolay ve keyifli okunuyor
Ek açıklamalar eklenmiş modern bir sürümü burada: https://data.jigsaw.nl/Rado_1962_OnNonComputableFunctions_Re...
Burada dikkat çeken nokta, ispatın bir Coq ispatı olması
Zaten bilinen bir ispatın bir teorem yardımcısına aktarılması değil de, baştan itibaren bir teorem yardımcısı içinde uygulanmış önemli bir ispat olarak ilk örnek olup olmadığını merak ediyorum. Daha önce bilgisayar destekli ispatlar vardı, ancak dört renk teoremi ya da Kepler varsayımı ancak daha sonra biçimsel doğrulama ortamlarına taşındı
Asıl sorun, karar vericilerin ve elle yapılan ispatların düzenli olmaması ve bir ölçüde şüpheli görünmesiydi. Özellikle Skelet #1’in nihai desene kadar hızlandırılması için özel bir programa ihtiyaç vardı [0], Skelet #17 için de Xu’nun durmadığını kanıtlamak üzere yoğun 7 sayfalık bir akıl yürütme yazması gerekmişti [1]. Tam Coq ispatı, bu sonuçların gerçekten ihtiyaç duyduğu güvenilirliği sağlıyor
[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
“Biçimsel doğrulama ortamı” ile tam olarak ne kastedildiğini anlamamış olabilirim, ama bildiğim kadarıyla dört renk teoremi en başından beri bilgisayarla kanıtlandı. Kempe’nin ilk ispat girişimi kusurluydu, ancak sonraki ispatta kullanılan temel araçlardan bazılarını sağladı; sonuçta teorem bilgisayarla kanıtlanmış gibi görünüyor
Bu Busy Beaver 1990’da keşfedildi ve 5 boyutundaki tüm makinelerin de kısa süre sonra listelenmiş olması muhtemel
Ekibi tebrik ederim. Artık boş bant temelinde 5 durumlu 2 sembollü Turing makinesi programları için durma problemi çözülmüş sayılır
Aynı tekniği 2 durumlu 4 sembollü duruma uygulamayı deneyen var mı merak ediyorum. Genel olarak semboller durumlardan daha güçlü olsa da, bu kadarı muhtemelen ele alınabilir gibi görünüyor ve şaşırtıcı sonuçlar da çıkabilir. 6 durumlu 2 sembollü ve 2 durumlu 5 sembollü durumların ikisi de zor görünüyor; hatta belki de kanıtlanabilir biçimde zor olabilir. Ayrıca, insanların zihnin gözüyle ya da beyindeki kuantum mekaniği gibi şeylerle durma probleminin cevabını sezebileceğine dair saçma ama tuhaf biçimde yaygın bir fikir var; elbette bu kanıtta böyle bir şey rol oynamadı
Bildiğim kadarıyla şu an kullanılan karar vericiler tek başına 2×4 için kalan tüm vakaların durmadığını kanıtlamaya yeterli. Dolayısıyla karar verici tasarımında büyük bir hata yoksa mevcut şampiyondan Σ(2,4) = 2.050, S(2,4) = 3.932.964 sonucu çıkıyor. Sadece sonuçlar tek bir yerde derlenmiş değil
2×5’te Hydra, 6×2’de ise Antihydra var; ikisi de yalnızca başlangıç noktası ve durma koşulu farklı olan aynı iterasyonu hesaplıyor. Standart varsayım, Mahler’in 3/2 problemiyle bağlantılı olarak bu iterasyonun mod 2’de eşdağılımlı olduğu; bu varsayım kanıtlanırsa 0 ve 1’in kümülatif oranı için üst ve alt sınırlar elde edilerek iki makinenin durmadığı neredeyse kesin biçimde kanıtlanabilir. Elbette bilinen bir kanıt yöntemi yok
Aleph* adlı mantık kuramı tabanlı bir kanıt üretici kullandı; o zamana gelindiğinde ZFC’nin BB(18)’i tesis edemeyeceği zaten 1.500 yıldır biliniyordu. 2024 ile karşılaştırıldığında, Aleph* kullanılmadan çok önceki hiçbir program teorik olarak bile BB(18)’i çözmek için kaba kuvvet kanıt denetiminde kullanılamazdı. Bu, bugün ZFC kanıtlarını sıralayıp denetleyerek teorik olarak BB(??)’yi çözebilmemizle tezat oluşturuyor
“İnsanların durma probleminin cevabını sezmesi” görüşüyle kastedilen bu. Bildiğim kadarıyla böyle bir gelecek tarihinin imkânsız olduğuna dair güçlü bir teorik neden yok. Ayrıca busy beaver hesaplanamaz olduğundan, gerekli programı yapmak için insanların yeni teoriler geliştirmesi gerekmişti. Sonucun kredisi bir şeye gitmeli; o dönemde program mevcut olmadığından bunu hesaplamaya yazamayız
Uzunluğu 5 olan tüm durmayan programların tesadüfen hepsinin durmadığının kanıtlanabilir olup olmadığını merak ediyorum
“Σ(5) = 1.915 ve S(5) = 2.358.064 olduğu gerçeği asla kanıtlanmayacak. Ya da daha büyük bir alt sınır bulunursa, bu tahmine o yeni değer konabilir.”
Gerekçesi, doğanın 5 durumlu beklemedeki makineler arasına Goldbach varsayımı kadar yakalanması zor en az bir problem yerleştirmiş olma ihtimalinin yüksek olmasıydı. Başka bir deyişle, bizim kavrama kapasitemizin ötesinde durmayan özyinelemeli örüntüler bulunma ihtimalinin yüksek olduğu anlamına geliyordu. Neyse ki bu öngörü gerçekleşmedi, ama fazladan sadece bir durumluk fark vardı
[0] Allen Brady, "The Busy Beaver Game and the Meaning of Life", Rolf Herken (ed.), The Universal Turing Machine: A Half-Century Survey içinde, Oxford University Press, 1988, ss. 259–277. Bu bölüm 2. baskıda da bulunabilir: Springer, 1995, ss. 237–254.
Pratik anlamdaysa başkaları zaten yanıtlamış. Matematiksel anlamdaysa BB(5) karar verilemez olsaydı epey şaşırtıcı olurdu. Çünkü 5 durumlu 2 sembollü makineler karar verilemez davranışı kodlamak için fazla küçük
Ancak eksiklik teoremlerinin sonucu olarak, standart matematiğin BB(n)’nin değerini kanıtlayamadığı bir n mutlaka vardır. Son yıllarda birkaç kişi böyle bir n bulup ne kadar düşürülebileceğini araştırdı; mevcut rekor[0] 745. Bu rekor muhtemelen daha da düşürülebilir, ama yine de bildiğimiz en yüksek değer 5 ile bilinemez olduğunu bildiğimiz en düşük değer 745 arasında büyük mesafe var
[0] “Standart matematik”in ne olduğunu merak edersin diye ekleyeyim: Bu, hem ZFC hem de PA için mevcut rekor. Yani en azından PA için daha da düşürmek mümkün olmalı gibi görünüyor. Şimdiye kadar PA’da ZFC’den daha iyi bir yöntem bulunamamış gibi, ama doğal olarak mümkün olması gerekmez mi?
“Sadece dört gün önce, mxdys ve Racheline adlı başka bir katkıcı BB(6) için aşılması zor görünen bir bariyer keşfetti. Bu, durma problemi Collatz varsayımı adlı ünlü derecede zor bir matematik problemine benzeyen 6 kurallı bir makine. Turing makineleri ile Collatz varsayımı arasındaki bağlantı matematikçi Pascal Michel’in 1993 tarihli makalesine kadar uzanıyor; ancak yeni keşfedilen ‘Antihydra’ adlı makine, matematikte kavramsal bir atılım olmadan çözülemez gibi görünen en küçük makine.”
Kişisel bir proje olarak kesim stoğu problemini (https://en.wikipedia.org/wiki/Cutting_stock_problem) çözen bir program yazmıştım
Stok; /---/, /---|, |---| biçimindeki parçaların kesimini içeriyordu ve 45 derece kesimlerde malzeme israf etmek istemediğim için mevcut programları kullanamıyordum ya da kullanmak istemiyordum. Brady’nin BB(4) aramasını optimize etmek için fark yaratmayan arama alt ağaçlarını budadığı açıklaması, benim programımı hızlandırırken yaptıklarıma oldukça benzediği için ilginç geldi
Scott Aaronson’ın blog yazısına göre 5 durumlu Turing makinesi sayısı 16.679.880.978.201
Bunların yüzde kaçının durduğunun bilinip bilinmediğini merak ediyorum. Düzenleme: n durumlu Turing makinesi sayısı (4n + 1)^(2n). Merak ettiğim analize benzer küçük n’ler için veri buldum: https://github.com/LukasKalbertodt/beaver
bbchallenge.org sitesinde bulamadım ama tüm makineler sınıflandırılmış durumda
Genel olarak bakıldığında kanıt oldukça kısa sayılır. Boşluklar ve yorumlar dahil 19.000 satır Coq
Deneyimlerime göre geleneksel bir makaleye derlense Coq sürümünden çok daha kısa olurdu. Elbette kanıtın uzunluğu zorluğun ya da karmaşıklığın ölçüsü değildir, ama çok kaba bir kıstas olarak kullanılabilir
İnsan bilgisinin sınırlarından söz ederken, kanıtlanabilir olsa da hiçbir insanın anlayamayacağı kadar karmaşık teoremleri sıkça düşünürüz. Muhtemelen elimizdeki en karmaşık kanıt sonlu basit grupların sınıflandırılmasıdır; binlerce, on binlerce sayfayı bulur ve dünyada tamamını bütünüyle anlayan çok az kişi vardır, hatta hiç kimse olmayabilir
Makalede söylendiği gibi BB(6) karar verilemez olabilir. Ancak milyonlarca sayfalık bir kanıtı olup insanlığın erişiminin dışında kalması da mümkün