An Alternative Approach to Formal Mathematics that Focuses on Communication and Accessibility

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

الفكرة الكبرى: طريقة جديدة لممارسة الرياضيات

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

الرياضيات الرسمية (Formal Mathematics) هي فكرة بناء هذه المدينة باستخدام مخططات صارمة، وقياسات دقيقة، ولغة عالمية حيث تُكتب كل قاعدة فيها بشكل صريح. الهدف هو القضاء على الغموض وضمان أن يكون كل شيء مثالياً من الناحية المنطقية.

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

---

المشكلة الحالية: نهج "المطلي بالذهب"

حالياً، الطريقة القياسية لممارسة الرياضيات الرسمية تشبه محاولة بناء منزل باستخدام مطرقة مطلية بالذهب.

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

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

---

الحل المقترح: النهج "الحر"

يقترح فارمر طريقة جديدة تسمى "النهج الحر" (Free Approach). فكر في هذا كالانتقال من المطرقة المطلية بالذهب إلى سكين الجيش السويسري (Swiss Army Knife).

يحافظ هذا النهج على دقة المنطق الرسمي ولكنه يزيل عبء فحص كل شيء بواسطة الحاسوب. إنه يركز على هدفين رئيسيين:

1. التواصل: جعل الرياضيات سهلة القراءة والفهم.
2. سهولة الوصول: جعلها سهلة الاستخدام لأي شخص، وليس فقط للخبراء.

إليك كيف يعمل "النهج الحر" باستخدام أربع قواعد بسية:

1. اللغة (R1)

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

2. الإثبات (R2)

في الطريقة القديمة، يجب عليك كتابة إثبات حاسوبي. في "النهج الحر"، يمكنك كتابة إثبات تقليدي (كما تفعل في ورقة بحثية أو كتاب).

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

3. التنظيم (R3)

تقترح الورقة تنظيم الرياضيات مثل مجموعة قطع الليغو (Lego) أو شبكة من الخرائط.

• تخيل أن لديك خريطة صغيرة لـ "المجموعة" (Monoid - بنية رياضية بسيطة). لست بحاجة لإعادة رسم تلك الخريطة في كل مرة تريد فيها التحدث عن "الأعداد الحقيقية".
• بدلاً من ذلك، تقوم بإنشاء "جسر" (يسمى تطابق نظرية أو theory morphism) يربط خريطة "المجموعة" بخريطة "الأعداد الحقيقية". يمكنك بعد ذلك "نقل" أفكارك من واحدة إلى الأخرى. هذا يمنعك من تكرار نفسك ويبقي كل شيء منظماً.

4. الأدوات (R4)

لا تحتاج إلى حاسوب خارق.

• المستوى 1: استخدم فقط LaTeX (أداة قياسية لكتابة الوثائق الرياضية).
• المستوى 2: استخدم برنامجاً مساعداً بسيطاً يفحص الأخطاء المطبعية.
• المستوى 3: استخدم "مساعد إثبات" كامل إذا كنت بحاجة إليه حقاً.
  المستخدم هو من يختار مقدار المساعدة التي يريدها.

---

المثال الواقعي: التفاضل والتكامل (Calculus)

تظهر الورقة مثالاً باستخدام التفاضل والتكامل (النهايات، المشتقات، التكاملات).

• الطريقة القديمة: سيتعين عليك كتابة كل تعريف للنهايات (limits) داخل الحاسوب بصيغة برمجية جامدة، وسيقوم الحاسوب بفحص كل خطوة منطقية.
• النهج الحر: تكتب تعريف النهاية باستخدام الرموز الرياضية القياسية التي تشبه الكتب الدراسية. تكتب الإثبات بطريقة يمكن للبشر قراءتها. يساعدك الحاسوب في تنظيم التعريفات ويضمن صحة الصيغة (syntax)، لكنه لا يجبرك على إثبات كل قفزة منطقية.

النتيجة؟ تحصل على وثيقة رياضية دقيقة (لا لغة غامضة فيها) ولكنها قابلة للقراءة (البشر يمكنهم فهمها).

لماذا نحتاج إلى هذا؟

يعتقد المؤلف أن للرياضيات الرسمية إمكانات هائلة:

• الدقة (Rigor): تمنعنا من ارتكاب أخطاء سخيفة.
• كشف الأخطاء: تلتقط الأخطاء المفاهيمية مبكراً (مثل مدقق إملائي للمنطق).
• دعم البرمجيات: تسمح للحواسيب بمساعدتنا في إجراء الرياضيات.
• التحقق (Verification): تمنحنا ثقة عالية في النتائج (وهو أمر بالغ الأهمية للأنظمة الحساسة للسلامة مثل أنظمة التحكم في الطائرات).
• الهيكلية: تحول الرياضيات إلى قاعدة بيانات منظمة وقابلة للبحث.

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

الخلاصة

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

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