بعد أكثر من 400 عام، حدث كيبلر صحيح

تخيل أنّ لديك عدداً كبيراً من ثمار البرتقال المدورة والمتساوية بالحجم، وتريد ترتيبها بشكلٍ معين، ما هي أفضل طريقة لتحقيق ذلك؟ أيّ طريقة تحقق لك وضع أكبر عددٍ ممكن من هذه الثمار في مكان ما؟
إنّ هذه المسألة، عزيزي المتابع، ليست سؤالاً للعمل في بقالة، وإنما هي مسألة رياضيّة قديمة لم يستطع أحد الإجابة عليها بشكل علميّ إلى أن جاء عالم الرياضيات الألماني Johannes Kepler واقترح عام 1611 أن البنية الهرميّة هي الشكل الأفضل، لأنها تحقق أكبر كثافة ممكنة، ولكنه لم يستطع إثبات ذلك.
والآن، بعد أكثر من 400 سنة أعلن الرياضيّ Hales Thomas، عالم الرياضيات من جامعة Pittsburgh فيPennsylvania، انتهاء جهوده المضنية لإثبات ما يدعى بحدس كيبلر.
إن عمل Hales لم يكن سهلاً أبداً، فقد كرّس الكثير من وقته من أجل هذا العمل حيث قدم في العام 1998 إثباتاً بأن حدس كيبلر كان صحيحاً. بالرغم من وجود عدد غير منته من الطرق التي يمكن بها ترتيب الأشكال المدورة، تمكن Hales قبل 16 عاماً من تقليص الإحتمالات إلى بضعة آلاف من الأشكال التي تمثل رياضياً العدد غير المنته من الترتيبات، وقام بالتحقق من هذه الإحتمالات باستخدام برمجيات معينة. ولكن الإثبات كان عبارة عن 300 صفحة، وتطلب عملاً متواصلاً لمدة 4 سنين من 12 اختصاصياً مدققاً للتحقق من صحته. وبالرغم من نشر البحث في المجلّة العلميّة Annals of Mathematics عام 2005 لم ينف المدققون إمكانيّة وجود خطأ في هذا الإثبات، حيث قالوا بأنهم "متأكدون بنسبة 99% من أن الحلّ صحيح".
في عام 2003 أطلق Hales مشروع Flyspeck للتأكد من إثباته حاسوبيّاً. وقد استعمل فريقه لهذا الغرض برنامجين حاسوبيين Isabelle و HOL Light يدعيان بـ proof software assistants، والذين يمكنان الحاسوب من التحقق من العبارات المنطقية والتأكد فيما إذا كانت صحيحة أم لا.
في يوم الأحد، الموافق ل 10 آب 2014 أعلن فريق Flyspeck انتهاءهم من تحويل النموذج الرياضي ل Hales إلى نموذجٍ حاسوبي تم التأكد من صحته.
يقول Hales: "إن التكنولوجيا المستخدمة في هذا العمل تنحيّ حكام الرياضيات جانباً.. آرائهم حول صحة إثباتي لم تعد مهمّة بعد الآن. أشعر بأن حملاً كبيراً أزيل عن عاتقي، أشعر بأني أصغر بعشر سنوات من عمري الحقيقيّ".
يقول Alan Bundy، أحد المشاركين في هذا العمل من جامعة Edinburgh في بريطانيا: "لقد بذلنا جهداً عظيماً. نأمل أن يلهم نجاح مشروعنا الرياضيين ليستخدموا الوسائل التكنولوجية للتحقق من الإثباتات الرياضيّة. إنّ هذه العملية، التي بدأت قبل 400 سنة كحدسٍ رياضيّ وانتهت بعمل حاسوبيّ ضخم، مهمة جداً. بالرغم من أنها ما زالت حالة شاذة فريدة، فإننا نأمل بأن تصبح المعيار الذي يتم العمل وفقه".

المصدر :
هنا