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

في وقت قريب، على رحلة قطار من ليون إلى باريس، جلس فلاديمير فيوفسكي إلى جانب ستيف أودي وحاول إقناعه بتغيير طريقته في الرياضيات.

فيوفسكي، في الرابعة والثمانين من عمره، عضو تدريس دائم في مؤسسة الدراسات المتقدمة في بريستون. ولد في موسكو ولكنه يتحدث الإنجليزية بطلاقة، ولديه ثقة من ليس مضطرًا إلى إثبات نفسه لأحد. في 2002 فاز بميدالية فيلدز التي تعتبر أكثر جائزة مرموقة في مجال الرياضيات.

الآن، وبينما يقترب القطار إلى المدينة، يخرج فيوفسكي حاسبه المحمول ويفتح برنامجًا اسمه Coq ، وهو برنامج مساعد في عملية الإثبات حيث يقدم للرياضيين بيئة يستطيعون بواسطتها كتابة الحجج الرياضية. أودي هو رياضي وعالم بالمنطق في جامعة كارنجي ميلون في بيتسبورغ، وباستخدام صياغة جديدة كان قد أنشأ ما يسمى بأسس أحادية التكافؤ univalent foundations . استطاع فيوفسكي كتابة تعريفها في 15 دقيقة، حيث قال في محاضرة ألقاها في الخريف الماضي أنه كان يحاول إقناع أودي باستخدام Coq لأداء الرياضيات، وأنها مهمة سهلة.

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

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

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

هذا أمر تعلمه فيوفسكي من خلال التجربة الشخصية. ففي عام 1999م اكتشف خطأ في ورقة كتبها قبل سبعة أعوام، وجد في الأخير طريقة لإنقاذ النتائج، ولكن في مقالة نشرها الصيف الماضي ضمن نشرة رسائل IAS كتب كيف أخافته هذه التجربة. بدأ يخشى أنه إذا لم يشكل عمله في الحاسب لن يمتلك ثقة كاملة في صحته.

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

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

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

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

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

“عليك أن تبني جسمًا معينًا وأن تلتزم به” كما قال أودي، وأضاف: ” إن أردت العمل مع جسم مختلف ولكن متماثل عليك أن تبينه من جديد.”

ولكن هذه النظرية ليست الطريقة الوحيدة لحل المسائل الرياضية. على سبيل المثال البرامج المساعدة في الإثبات Coq و Agda مبنية على نظام أساسي آخر يسمى نظرية النوع.

نظرية النوع تعود أصولها إلى محاولة لحل الشائب الحرج في النماذج الأولية من نظرية الزمر، والتي تم تعريفها عن طريق الفيلسوف والعالم بالمنطق برتراند راسل عام 1901 حيث نبه أن بعض الزمر تحتوي على أنفسها كأعداد. مثلًا؛ تخيل زمرة تحتوي على الأشياء التي ليست سفنًا فضائية. هذه الزمرة – من الزمر التي لا تحتوي على سفن فضائية – لا تحتوي هي نفسها على سفن فضائية، وبالتالي فهي رقم داخل نفسها.
راسل قام بتعريف زمرة جديدة: زمرة كل الزمر التي لا تحتوي على نفسها. وتساءل عن ما إذا كانت هذه الزمرة تحتوي على نفسها، ووضح أن إجابة هذا السؤال تحتوي على مفارقة: إن لم تحتوي الزمرة على نفسها فهي إذَا لا تحتوي على نفسها لأن كل الأشياء الوحيدة الموجود فيها هي زمر لا تحتوي على نفسها. ولكن إن لم تحتوِ على نفسها فهي تحتوي على نفسها لأن الزمرة تحتوي كل الزمر التي لا تحتوي على نفسها.

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

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

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

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

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

النقطة والخط هما مثلي التواضع متماثلان، وهي طريقة أخرى لقول أنهما من نفس نوع التوبولوجي. الحرف p والحرف o كذلك، ويتشاركان ذلك مع بقية حروف الأبجدية التي لها فراغ واحد A , Q , D, R .

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

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

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

فيوفسكي عاد إلى هذه المعضلة بعد أن فاز بجائزة الميدلفيلدز في أواخر 2005. سرعان ما بدأ التفكير بهذه العلاقات من درجات أعلى في حدود الأجسام التي تسمى لا نهائية – قروبويدز بدأت الأشياء تتوضح له. هذه الأجسام ترمّز (كتابة أكواد) كل المسارات في فراغ، من ضمنها المسارات بين المسارات والمسارات التي بين المسارات بين المسارات. وهي تنشأ في أبحاث أخرى من الرياضيات كوسيلة لترميز علاقات من درجات أعلى مماثلة. بسبب هذا اعتبرها فيوفسكي بلا قيمة بالنسبة لهدفه النهائي وهو إعادة تشكيل الرياضيات.

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

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

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

ففي عام 1972 قدّم عالم المنطق السويدي بير ماتين – لوف نسخته الخاصة من نظرية النوع التي استمدها من أفكار لغة البرمجة الرسمية لتدقيق الإثباتات على الحواسيب Automath. ونظريته MLTT تم تبنيها بشكل واسع بواسطة علماء الحواسيب الذين استخدموها كأساس للبرامج المساعدة في الإثبات.

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

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

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

وقد توصّل لهذا الرابط عندما قرأ ورقة ماكاي، واستغرقه جعلها محكمة رياضيًا 4 سنوات. من 2004 حتى 2009 طور عدة أجزاء من آليات تسمح للرياضيات أن يعملوا مع الزمر بواسطة MLTT “بطريقة محكمة ومناسبة للمرة الأولى” كما قال. تضمّن هذا مسلمة جديدة تعرف بمسلمة وحدة التكافؤ، وتفسير كامل لـMLTT باعتبار تشكيل جبري بحت في النظرية simplicial sets يعد نموذجًا من مفهوم يحتوي الفراغات التوبولوجية حسنة التصرف، والتي بالإضافة للقروبويدز تعتبر وسيلة أخرى لتمثيل الأنواع مثلية التوضع. وقد أشار دانييل جريسون أن قوة الأسس وحيدة التكافؤ تكمن في واقع أنها تشير إلى نظام خفي سابق في الرياضيات، حيث يتضح أن أفكارًا من التوبولوجي تأتي من أسس مختلفة من الرياضيات.

من الفكرة إلى العمل
بناء أسس جديدة للرياضيات شيء، و جعلها متداولة بين الناس شيء آخر. بأواخر 2009 بدأ فيوفسكي العمل بتفاصيل الأسس أحادية التكافؤ وشعر بجاهزيته لمشاركة أفكاره. فَهِم أن الناس سيكونون متشككين على الأغلب. ” إنه أمر ضخم أن أقول أن لدي شيء يجب أن يستبدل نظرية الزمر.” كما قال.

بدأ فيوفسكي بمناقشة الأسس أحادية التكافؤ للمرة الأولى علنًا في محاضرة ببداية 2010 في كارنيج ميلون وفي مؤسسة أوبرولفاخ للبحوث الرياضية في ألمانيا سنة 2011. في الأولى تكلم عن لقائه بستيف أودي الذي كان يقوم بأبحاثه مع طلاب الدراسات العليا بخصوص نظرية مثلية التوضع النوعية. بعدها بفترة، قرر فيوفسكي أن يقرب الأبحاث من بعضها لفترة لاجتماع مكثف بسبيل بدء تطور الحقل.
بشراكة ثيري كوقواند، عالم حاسوب من جامعة جوثنبرج في السويد، قام فيوفسكي وأودي بتنظيم بحث السنة المميز ليقام في IAS خلال سنة 2012- 2013 الأكاديمية. أكثر من 30 عالم حاسوب، وعالم بالمنطق والرياضيات أتوا من أنحاء العالم للمشاركة. قال فيوفسكي: ” لم يكن هناك أحد مرتاح مع الفكرة بشكل تام.”

بدت الفكرة غريبة قليلًا لكنهم كانوا متشوقين. أجّل شولمان بداية وظيفة جديدة ليكون جزءًا من المشروع ” أظن أن كثيرًا منا شعر أننا على مشارف شيء ضخم، شيء مهم للغاية وكان الأمر يستحق القيام ببعض التضحية.”

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

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

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

“إن الانقياد نحو الإثبات الميكانيكي والتحقق من الإثباتات لا تحفز كثيرًا من الرياضيين حسبما أظن” وأضاف ” أفهم حماس علماء المنطق والحاسوب ولكن أظن أن الرياضيين يبحثون عن شيء مختلف”.

يدرك فيوفسكي أن أسس جديدة للرياضيات صعبة القبول، ويعترف بذلك “في هذه اللحظة هناك كثير من الضوضاء والصخب التي لم يستعد لها المجال بعد”. فهو حاليًا يستخدم لغة الأسس أحادية التكافؤ لإعادة تشكيل العلاقة بين MLTT ونظرية مثلية التوضع، ويعتبرها خطوة مهمة لتقدم المجال. ولديه أيضًا خطط لتشكيل إثباته الذي اكتسب بسببه ميدالية فيلدز (Milnor conjecture) ويأمل أن فعل هذا سيبدو وكأنه “خطوة يمكن استخدامها لتكوين تحفيز في المجال” ويرغب أن يقوم بالنهاية باستخدام الأسس أحادية التكافؤ لدراسة جوانب الرياضيات التي أصبح من الصعب الوصول إليها من خلال إطار عمل يعتمد على نظرية الزمر. ولكن حاليًا يقوم بالاقتراب من تطور الأسس أحادية التكافؤ بحذر.
دعمت نظرية الزمر الرياضيات لأكثر من قرن، وإذا أتيح للأسس أحادية التكافؤ زمنًا ممثلًا، يدرك فيوفسكي أن من المهم أن تكون الأشياء سليمة منذ البداية.

ترجمة: آلاء المشيقح
Kendahkhalil
مراجعة: ميسم الفداغ
المصدر:
https://www.quantamagazine.org/20150519-will-computers-
redefine-the-roots-of-math/