المحرر العلمي 
قد يبدو السؤال بسيطًا، ولكنه يثير خلافًا بين الرياضياتيين، إذ لا توجد له إجابة محددة وواضحة. وتنعكس هذه الإشكالية على دقة استخدام الحواسيب في التحقق من صحة البراهين الرياضياتية. وربما يكمن الحل في إعادة بناء الأسس التي تقوم عليها الرياضيات بالكامل.
عندما نقرأ المعادلة «2 + 2 = 4»، ما الذي يعنيه الرمز «=»؟ هذا السؤال أكثر تعقيدًا مما يبدو؛ إذ لا يوجد اتفاق بين علماء الرياضيات على تعريف دقيق لما يجعل شيئين متساويين. وعلى الرغم من أن هذا الجدل ظل على نار هادئة ضمن الأوساط المختصة لعقود من الزمان، فإن التوجّه الحديث نحو جعل البراهين الرياضياتية قابلة للتحقّق بوساطة برامج الحاسوب، وهو ما يُعرف في الأوساط المتخصصة بالتشكيل الرياضياتي Formalisation، أعاد تسليط الضوء على هذا الجدل.
يقول كيفن بَزارد Kevin Buzzard، من جامعة إمبريال كوليدج لندن Imperial College London: «يستخدم الرياضياتيون مفهوم التساوي بمعنيين مختلفين، وكنت أتقبلُ ذلك، إلى أن بدأتُ في أداء العمليات الرياضياتية باستخدام الحاسوب». ويضيف أن العمل مع برامج مساعدة على إثبات البراهين الرياضياتية بوساطة الحاسوب جعله يُدرك أنَّ على علماء الرياضيات حاليًّا التعامل مع غموضٍ كان مفيدًا حتى وقت قريب، وقد يدفعهم ذلك إلى إعادة صياغة الأسس النظرية التي تقوم عليها الرياضيات بصورة جذرية.
المعنى الأول للتساوي مألوف لمعظم الرياضياتيين، ويُفهَم على أنه يعني أن طرفي المعادلة يمثلان الكيان الرياضياتي ذاته، ويمكن إثبات ذلك عبر سلسلة من التحويلات المنطقية من أحد الطرفين إلى الآخر. وعلى الرغم من أن الرمز «=» لم يظهر إلا في القرن السادس عشر، فإن هذا المفهوم للتساوي يعود إلى العصور القديمة.
لكن في أواخر القرن التاسع عشر، بدأت الأمور تتغير مع نشوء نظرية المجموعات Set theory التي أرست الأسس المنطقية لمعظم الرياضيات الحديثة. وتُعنى نظرية المجموعات بدراسة مجموعات من الكيانات الرياضياتية، وقد قدّمت تعريفًا إضافيًّا لمفهوم التساوي: إذا احتوت مجموعتان على العناصر ذاتها، فهما متساويتان، وهو تعريف ينسجم – في جوهره – مع المفهوم الرياضياتي التقليدي. مثلًا، تُعدّ المجموعتان {1، 2، 3} و{3، 2، 1} متساويتين؛ لأن ترتيب العناصر داخل المجموعة ليس ذا تأثير.
لكن، مع تطور نظرية المجموعات، يقول بزارد بدأ بعض الرياضياتيين يقولون إن مجموعتين تُعدّان متساويتين إذا وُجدت بينهما طريقة واضحة للمطابقة، حتى إن لم تحتويا على العناصر ذاتها تمامًا.
لفهم ذلك، تأمّل المجموعتين {1، 2، 3} و{a، b، c}. من الواضح أن عناصر كل مجموعة مختلفة، وبالتالي فهما غير متساويتين. غير أن هناك طرقًا لإيجاد تطابق بين عناصر المجموعتين، من خلال إقران كل حرف برقم. ويُطلِق علماء الرياضيات على هذا النوع من المطابقة مصطلح التماثل البنيوي Isomorphism. وفي هذه الحالة، هناك عدة تماثلات بنيوية ممكنة؛ لأن لدينا خيارات متعددة لتعيين رقم لكل حرف، لكن في كثير من الحالات، لا يكون هناك إلا اختيار واحد واضح وطبيعي، يُعرف بـالتماثل البنيوي القياسي Canonical Isomorphism.
وبما أن التماثل البنيوي القياسي بين مجموعتين هو الطريقة الوحيدة الممكنة للربط بينهما، فإن العديد من الرياضياتيين صاروا يعدونه دليلًا على أن المجموعتين متساويتان، على الرغم من أن هذا المفهوم لا يطابق – من الناحية التقنية – مفهوم التساوي الذي نألفه. يقول بَزارد: «هاتان المجموعتان تتطابقان بطريقة طبيعية تمامًا، وقد أدرك علماء الرياضيات أنه سيكون من العملي جدًّا التعامل معهما على أنهما متساويتان».
وجود تعريفين مختلفين لمفهوم التساوي لا يطرح مشكلة حقيقية لعلماء الرياضيات عند كتابة الأوراق العلمية أو إلقاء المحاضرات؛ إذ يكون المعنى واضحًا دائمًا من السياق، غير أن الأمر يطرح مشكلات أمام برامج الحاسوب التي تحتاج إلى تعليمات دقيقة صارمة، على ما يقول كريس بركبِك Chris Birkbeck، من جامعة إيست أنغليا University of East Anglia في المملكة المتحدة. ويضيف: «لقد أدركنا أننا كنا، إلى حدٍّ ما، متساهلين بعض الشيء طوال الوقت، وربما ينبغي علينا تصحيح بعض الأمور».
ومن أجل معالجة ذلك، يعكف بَزارد على دراسة الطريقة التي يستخدم بها بعض علماء الرياضيات التماثل البنيوي القياسي بوصفه مساواة، وما يُمكن أن يترتب على ذلك من مشكلات عند التعامل مع أنظمة البرهان الحاسوبي ذات القواعد المنهجية الدقيقة.
تُعدّ أعمال ألكسندر غروتنديك Alexander Grothendieck، أحد أبرز علماء الرياضيات في القرن العشرين، من أكثر الأعمال تعقيدًا، والتي تتعذر حاليًا صياغتها ضمن إطار رسمي دقيق يتيح تحويلها إلى لغة رياضياتية منطقية صارمة، تمكّن أنظمة البرهنة الحاسوبية من التحقق من صحتها. يقول بَزارد: «لا تستطيع الأنظمة الحالية تمثيل الطريقة التي يستخدم بها علماء مثل غروتنديك رمز التساوي بصيغة منطقية دقيقة ومفهومة رياضيًّا».
وتكمُن جذور هذه المشكلة في الطريقة التي يُنشئ بها علماء الرياضيات براهينهم؛ إذ يتطلّب الشروع في إثبات أي شيء، افتراض مجموعة من المسلّمات Axioms، وهي فرضيات تُؤخذ على أنها صحيحة من دون الحاجة إلى برهان، وتُوفّر إطارًا منطقيًّا يُبنى عليه الاستدلال. ومنذ أوائل القرن العشرين، استقر علماء الرياضيات على مجموعة من المسلّمات، ضمن نظرية المجموعات، تُشكّل أساسًا راسخًا لبنية الرياضيات. وبناءً على ذلك، لا يحتاجون – عادةً – إلى الرجوع المباشر إلى تلك المسلّمات في ممارساتهم اليومية؛ إذ يُفترَض أن الأدوات الرياضياتية المُستخدَمة عمومًا تعمل بصورة صحيحة، على نحوٍ يُشبه عدم انشغالك بالتفكير في تفاصيل مطبخك الداخلية قبل إعداد وجبة الطعام.
يقول بركبِك «بصفتك عالم رياضيات، فأنت تدرك جيدًا ما تفعل إلى درجة أنك لا تُعير الأمر كثيرًا من الانتباه». إلا أن هذا النهج ينهار عند إدخال الحواسيب طرفًا في العملية؛ فهي ستُنفّذ العمليات الرياضياتية حينها بطريقة تُشبه بناء مطبخ كامل من الصفر، في كل مرة تُعد فيها وجبة. ويُضيف بركبِك: «بمجرد أن يبدأ الحاسوب في التحقّق من كل ما تقول، لا يعود في إمكانك التحدث بعبارات غامضة على الإطلاق، بل يتعيّن عليك أن تتوخى الدقة التامة في كل ما تقول».
لحل هذه الإشكالية، يرى بعض علماء الرياضيات أنه ينبغي إعادة تعريف الأسس النظرية للرياضيات؛ بحيث يصير التماثل البنيوي القياسي والتساوي شيئًا واحدًا لا فرق بينهما. ويمكن عندها برمجة أنظمة الحاسوب للعمل وفق هذا التصور الجديد. يقول تورستن ألتِنكيرش Thorsten Altenkirch، من جامعة نوتنغهام University of Nottingham في المملكة المتحدة: «إن التماثل البنيوي هو التساوي… أعني، ماذا يمكن أن يكونا؟ إذا لم يكن في الإمكان التمييز بين كيانين متماثلين بنيويًّا، فماذا لدينا غير ذلك؟ وما الذي يمكن أن نطلقه على هذه العلاقة بينهما؟».
تُبذَل حاليًا جهودٌ لتنفيذ ذلك ضمن فرع رياضياتي يُعرف باسم نظرية الأنماط التماثلية Homotopy type theory التي تُعرِّف كلًّا من التساوي التقليدي والتماثل البنيوي المقياسي على نحو متطابق. ويقول ألتِنكيرش إنه، بدلًا من محاولة تعديل أدوات إثبات البراهين القائمة لتتلاءم مع مفهوم التماثل البنيوي القياسي، ينبغي لعلماء الرياضيات اعتماد نظرية الأنماط، واستخدام أنظمة إثبات بديلة تتوافق معها مباشرة.
أما بَزارد، فلا يؤيد هذا الطرح، لا سيما بعد أن بذل جهدًا كبيرًا في استخدام الأدوات المتاحة حاليًا لتشكيل براهين رياضياتية ضرورية للتحقق من أعمال أكثر تقدمًا، مثل مبرهنة فيرما الأخيرة Fermat’s last theorem. وهو يرى أن مسلّمات الرياضيات ينبغي أن تبقى كما هي، وأن الحل يتمثل في تعديل الأنظمة الحالية بدلًا من تبنّي نظرية الأنماط. ويقول بَزارد: «ربما يكمن الحل الأفضل في ترك الباحثين في الرياضيات على ما هم عليه؛ فمن الصعب جدًّا تغييرهم؛ ما يجدر بنا أن نفعل هو تحسين أنظمة الحاسوب».
