حدسية ABC: المشروع السري لتسوية البرهان الرياضي المثير للجدل باستخدام الكمبيوتر

قد يكون أحد البراهين الأكثر إثارة للجدل في الرياضيات الحديثة على وشك أن يتم حله. هناك مشروعان، يهدف كل منهما إلى استخدام برنامج كمبيوتر لإلقاء ضوء جديد على هذا الجدل، وقد تم الآن تشغيلهما ــ أحدهما يعمل سراً منذ أكثر من عامين بالفعل. وتعتبر هذه التطورات علامة إيجابية على أن الخلاف قد يجد حلاً، كما يقول علماء الرياضيات.

بدأت القصة في عام 2012 عندما ادعى شينيتشي موتشيزوكي، من جامعة كيوتو باليابان، أنه أثبت فكرة مشهورة تسمى حدسية ABC، وقام بنشر دليل من 500 صفحة على الإنترنت. التخمين سهل الطرح، فيما يتعلق بالأعداد الأولية المشاركة في حلول المعادلة a + b = c وكيفية ارتباط هذه الأرقام ببعضها البعض. لكن حلها يتطلب رؤى عميقة حول طبيعة كيفية تفاعل الجمع والضرب. للإجابة أيضًا آثار بعيدة المدى على التخصصات الرياضية الأخرى.

كان برهان موتشيزوكي بمثابة قنبلة رياضية، ولكن كان من الصعب على العديد من زملائه فهمه لأنه أظهر تقنيات ومفاهيم جديدة، والتي أطلق عليها بشكل جماعي نظرية تيشمولر بين الكون (IUT). أمضى علماء الرياضيات البارزون الأشهر التالية في محاولة توضيح عمل موتشيزوكي، بما في ذلك في المحادثات مع موتشيزوكي نفسه، لكن صحة الدليل وصلت إلى طريق مسدود.

في عام 2018، بعد أن أعلن اثنان من علماء الرياضيات البارزين – بيتر شولز من جامعة بون وجاكوب ستيكس من جامعة جوته في فرانكفورت، وكلاهما في ألمانيا – أنهما حددا خطأ محتملا، لم يكن هناك أي تقدم آخر. أكد موتشيزوكي وعدد من زملائه المقربين، معظمهم في جامعة كيوتو، أن الدليل كان صحيحًا، في حين جادل جزء أكبر من المجتمع الرياضي بأن الدليل كان في أحسن الأحوال غير قابل للفك، وفي أسوأ الأحوال معيبًا بشكل قاتل.

ولكن في العام الماضي، عرض موتشيزوكي غصن زيتون على الرافضين وطريقاً محتملاً للمضي قدماً. كان هناك تقدم هائل في مجال الرياضيات الذي يسمى إضفاء الطابع الرسمي، حيث تتم ترجمة البراهين الرياضية المكتوبة إلى لغة كمبيوتر يمكنها التحقق من صحتها تلقائيًا. وكانت إحدى اللغات المحددة، والتي تسمى Lean، هي الأكثر جذبًا لموتشيزوكي. وكتب في ذلك الوقت أن: “(اللين) هو التكنولوجيا الأفضل وربما الوحيدة… لتحقيق تقدم ملموس فيما يتعلق بالهدف الأساسي المتمثل في تحرير الحقيقة الرياضية من نير الديناميكيات الاجتماعية والسياسية”.

الآن، الجهود المبذولة لإضفاء الطابع الرسمي على برهان موتشيزوكي لحدسية ABC في اللين جارية رسميًا، مع إعلان مجموعتين رياضيتين منفصلتين على الأقل عن التقدم، بما في ذلك مجموعة يقودها موتشيزوكي وأخرى تعمل سرًا لأكثر من عامين، لكنها وصلت إلى طريق مسدود.

في أواخر عام 2023، بدأ كاتو فوميهارو في مركز ZEN للرياضيات في اليابان مشروع الهندسة اللينة والأنابيلية (LANA)، حيث قام بتجنيد علماء الرياضيات الذين كانوا على دراية بعمل موتشيزوكي بالإضافة إلى خبراء في اللينة الذين أضفوا الطابع الرسمي على مشاريع رياضية كبيرة أخرى. كان الهدف الأساسي هو “تسوية الخلاف مرة واحدة وإلى الأبد”، كما يقول آدم توباز من جامعة ألبرتا بكندا، الذي جنده فوميهارو للمساعدة في إضفاء الطابع الرسمي على الدليل.

وفي مؤتمر صحفي عُقد الشهر الماضي للإعلان عن المشروع، قال فوميهارو إن الأعضاء توصلوا إلى “فهم عميق” لفكرة موتشيزوكي خلال السنوات القليلة الماضية، ولكن كانت هناك أيضًا نقطة محددة لم يتمكنوا من التقدم فيها، وهي مرتبطة ارتباطًا وثيقًا بالمجال الذي حدده شولز وستيكس على أنه يحتوي على خطأ محتمل في عام 2018. يقول توباز: “لقد تعثرنا بشكل أساسي في محاولة فهم نقطة معينة في IUT”. “لقد عزلنا هذه النقطة منذ ما يقرب من عام ونصف الآن، واعتقدنا في الأصل أننا بحاجة فقط إلى فهم المزيد من النظرية حتى نتمكن من تجاوز هذه المشكلة المحتملة.”

ولكن حتى بعد محاولة فهم الأمر من خلال ورش العمل المختلفة والتواصل غير المباشر مع موتشيزوكي عبر وسيط، لم يتمكن فوميهارو وزملاؤه من إحراز تقدم.

وفي تطور منفصل، بدأ موتشيزوكي وزملاؤه أيضًا مشروعًا لإضفاء الطابع الرسمي على الدليل باستخدام اللين. لكنهم أقل اهتمامًا بإثبات صحتها، حيث يؤكد موتشيزوكي أنها صحيحة بالفعل. وبدلاً من ذلك، فهو يرى قيمة المشروع أكثر في التواصل.

وقال موتشيزوكي في مؤتمر عُقد مؤخرًا في جامعة إكستر بالمملكة المتحدة: “إن جانب التحقق هذا ليس نقطة اهتمام مركزية”. “تكمن أهمية إضفاء الطابع الرسمي على Lean في إنتاج سجل دقيق للبنية المنطقية لـ IUT التي تكون محصنة ضد التفسيرات الخاطئة، وبالتالي يمكن استخدامها لإيصال هذه البساطة بطريقة فعالة أو دقيقة إلى أقصى حد لعلماء الرياضيات الآخرين.”

يتمثل نهج موتشيزوكي وفريقه في التركيز على المنطقة المثيرة للجدل المتمثلة في الدليل الذي أصبح مشروع LANA عالقًا فيه، والذي حدده شولز وستيكس لأول مرة، قبل الانتقال إلى إضفاء الطابع الرسمي على مخطط بأربع مراحل أخرى. يدعي Mochizuki أنهم بدأوا في القيام بذلك من خلال إنتاج 70 سطرًا من كود Lean كبداية، على الرغم من أنها ليست متاحة للعامة بعد.

يقول كيفن بوزارد من جامعة إمبريال كوليدج في لندن، إن هذا لا يمثل الكثير من التعليمات البرمجية. “سيكون أكثر بكثير من 70 سطرًا. عند 70 سطرًا، ستواجه صعوبة في إثبات بعض النظريات على مستوى المرحلة الجامعية، ناهيك عن إثبات ضخم.”

ومع ذلك، لا يزال هذا أحد أكثر التقدمات الواعدة والأكثر أهمية في فهم برهان موتشيزوكي منذ الإعلان عنه لأول مرة. يقول بوزارد: “لم تكن هناك أي حركة، ولم تكن هناك معلومات جديدة مثيرة للاهتمام ذات صلة على الإطلاق، وهذه هي المرة الأولى التي تشعر فيها أن الأمور ربما تتحرك بالفعل”.

يوافق توباز على أنه على الرغم من الصعوبات، لا يزال هناك طريق محتمل للمضي قدمًا، خاصة وأن موتشيزوكي كان يتواصل علنًا مع مشروع LANA، على الرغم من أن جهود المجموعات ظلت متميزة.

يقول توباز: “الآن بعد أن أصبح هذا الحوار مع موتشيزوكي باستخدام نهج Lean، فأنا في الواقع متفائل جدًا بإمكانية التوصل إلى حل لهذا الجدل”. “إذا كان هناك أي شيء يمنحني أكبر قدر من التفاؤل في هذه المرحلة، فهو أننا نجري هذا الحوار ذهابًا وإيابًا مع مجموعة موتشيزوكي.”