لعبة القندس المشغول

لعبة القندس المشغول هي مشكلة نظرية في علوم الكمبيوتر اقترحها عالم الرياضيات تيبور رادو في عام 1962. تتضمن اللعبة نوعًا خاصًا من آلات تورينج يسمى "القندس المشغول"، وهو برنامج مصمم لكتابة أكبر عدد ممكن من "1" على قطعة طويلة بلا حدود من شريط الورق. في لعبة Busy Beaver، بالنظر إلى عدد صحيح موجب، ضع في اعتبارك جميع آلات تورينج مع الحالات (بما في ذلك أبجدية الإدخال ووظيفة انتقال الحالة، وما إلى ذلك). هدف اللعبة هو العثور على آلة تورينج التي، عند إعطاء إدخال فارغ، تستغرق أطول وقت (أو أكبر عدد من الخطوات) قبل التوقف، مع إخراج أكبر عدد من 1. عدد 1 في هذا الإخراج هو قيمة دالة القندس المشغول المقابلة للعدد الصحيح الموجب، والذي يشار إليه بـ BB(n)، حيث n هو عدد حالات آلة تورينج.

في سبتمبر 2024، أعلن فريق مكون من أكثر من 20 مساهمًا أنهم عثروا على رقم القندس الخامس المزدحم، BB(5)، بقيمة 47,176,870. هذه النتيجة هي جزء من مشروع Busy Beaver Challenge الذي بدأه تريستان ستيرين، وهو تعاون عبر الإنترنت يهدف إلى تحديد قيمة BB(5) في النهاية. وقد تحقق الفريق من نتائجهم باستخدام برنامج يسمى مساعد إثبات Coq، وهي أداة تحقق رسمية تستخدم لضمان دقة البراهين الرياضية.