يجتمع عشرات من علماء الرياضيات على الإنترنت بواسطة برنامج يُسمَّى بـ“زوليب – Zulip” لبناء ما يُفيدهم مستقبلًا في مجالهم، كما يُفضِّلون برنامج “لين – Lean” لقدرته على مساعدة العلماء في كتابة البراهين الرياضية. ولكن لكي يقوم برنامج (لين) بذلك، يجب على العلماء إدخال العمليات الرياضية بأنفسهم، وترجمة آلاف السنين من المعرفة إلى نموذج يمكن أن يفهمه برنامج (لين).
يقول “كيفن بازارد – Kevin Buzzard”، أستاذ الرياضيات البحتة في “كلية لندن الإمبراطورية – Imperial College London”: “يتضح أنه عند القيام برقمنة شيء ما، يمكن استخدامه بطرق جديدة. سوف نقوم برقمنة الرياضيات، وهذا سيجعلها أفضل مما هي عليه الآن”.
رقمنة الرياضيات حلم يسعى إليه العلماء منذ فترة طويلة. أما عن فوائد رقمنة الرياضيات، فقد تتراوح الفوائد المتوقعة من الأمور العادية؛ كتقييم الواجبات المنزلية للطلاب، وصولًا إلى الاستخدام الأمثل لها والأكثر فائدة، كاستخدام الذكاء الاصطناعي لاكتشاف رياضيات جديدة، وإيجاد حلول جديدة لمشاكل قديمة قد سبق الكشف عنها.
يتوقع العلماء أن برامج “مُساعدي البُرهان – proof assistants” -يُعَدُّ مساعد البرهان أداة برمجية للمساعدة في تطوير البراهين الرسمية عن طريق التعاون بين الإنسان والآلة- يمكنها مراجعة بعض العمليات الرياضية، واستكشاف أخطاء قد لا يكتشفها العنصر البشري أحيانًا، والتعامل مع الأعمال التقنية المملة التي تأخذ وقتًا طويلًا.
لكن أولًا، يجب على علماء الرياضيات -عند عقد اجتماعاتهم على برنامج (Zuilp)- تزويد برنامج (لين – Lean) بمعلومات لازمة تتوافق مع مكتبة المعرفة الرياضية الجامعية. ولكن لا يزال العلماء في منتصف طريق حلمهم؛ فلن يستطيع برنامج (لين) حل جميع المشاكل الرياضية في أي وقت حاليًا، ولكن من المتوقَّع من العلماء الذين يعملون على تطويره أنه في خلال سنوات سيكون البرنامج قادرًا على فهم أسئلة امتحانات طلاب السنوات النهائية. وبعد ذلك، لا يدري علماء الرياضيات المشاركون في هذه الجهود تمامًا ما ستكون الرياضيات الرقمية مفيدة له.
خلال فصل الصيف، أدارت مجموعة من مستخدمي برنامج (لين) ذوي الخبرات الكبيرة ورشة عمل عبر الإنترنت بعنوان “Lean for the Curious Mathematician”. وفي الجلسة الأولى، شَرح “سكوت موريسون – Scott Morrison” -من “جامعة سيدني University of Sydney”- كيفية كتابة الإثباتات الرياضية وتزويد البرنامج بها.
بدأ (سكوت موريسون) بكتابة الجملة التي يريد إثباتها بالطريقة التي يفهمها برنامج (لين) باللغة الإنجليزية، تُترجَم إلى “هناك عدد لا نهائي من الأعداد الأولية”، وهناك عدة طرق لإثبات صحة هذه الجملة، لكن (موريسون) أراد استخدام تعديل طفيف لأول شخص أثبت هذا -وهو (إقليدس)- منذ عام 300 قبل الميلاد، والذي يتضمن ضرب جميع الأعداد الأولية المعروفة معًا، وإضافة رقم 1 للعثور على عدد أولي جديد. عكَسَ اختيار العالم (موريسون) شيئًا أساسيًا حول استخدام برنامج (لين)، حيث يجب على المستخدم أن يبتكر فكرة كبيرة عن الإثبات بمفرده.
بعد كتابة (موريسون) الجملة التي يريد إثباتها، استغرق بضع دقائق في وضع الأساسيات التي يُبنَى عليها الإثبات، وقد حدد مجموعة من الخطوات التي سوف تُتَّبَع،. وفي نفس التوقيت، برنامج (لين) لا يمكنه الوصول إلى الاستنتاجات الكاملة بسهولة؛ بل يمكن أن يساعد في تنفيذ خطوات بسيطة وسهلة الفهم. يقوم برنامج (لين) ببعض العمليات باستخدام نظام يُسمَّى “التكتيكات”، وهو عبارة عن خوارزميات قصيرة مصمَّمة لأداء وظيفة محددة للغاية.
أثناء قيام العالم (موريسون) بعمله في إثباتاته الرياضية، نفَّذ تكتيكًا آخر يُسمَّى “البحث في المكتبة”، واستطاع البحث في قاعدة بيانات برنامج (لين) للنتائج الرياضية، وأعاد البرنامج بعض النظريات التي اعتُقِد أنها يمكن أن تملأ تفاصيل جزء معين من الإثبات.
كما اكتشف أيضًا تكتيكًا آخر يُسمَّى “ليناريث – Linarith” يؤدي مهام رياضية مختلفة، حيث يُمكن أن يأخذ مجموعة من المتباينات (على سبيل المثال، رقمين حقيقيين) ويوضح لك أنها متباينة جديدة تتضمن رقمًا ثالثًا صحيحًا (فإذا كان: “أ” هو 2، “ب” أكبر من “أ”، فإن “4ب” + “3أ” أكبر من 12)، كما يستطيع البرنامج القيام بمعظم عمليات القواعد الجبرية الأساسية.
استغرق (موريسون) 20 دقيقة لاستكمال إثبات نظرية (إقليدس). وفي بعض الأوقات، استخدم تكتيكات معينة في كل خطوة أثناء استكماله لإثبات (إقليدس). في كل خطوة، كان يفحص برنامج (لين) للتأكد من أن عمله يتوافق مع القواعد المنطقية الأساسية للبرنامج، والتي تمَّت كتابتها بلغة رسمية تُسمَّى “نظرية النوع”.
كانت عملية الإثبات شيقة، كما هو الحال دائمًا عندما تتدخل التكنولوجيا للقيام بشيء اعتاد الإنسان القيام به، ولكن إثبات (إقليدس) موجود منذ أكثر من 2000 عام. أنواع المشاكل التي يهتم بها علماء الرياضيات اليوم معقدة للغاية، لدرجة أن برنامج (لين) لا يستطيع فهم جميع الأسئلة حتى الآن. ولذلك، قبل أن يتمكن علماء الرياضيات اليوم من العمل من خلال برنامج (لين) في حل المشكلات التي يهتمون بها، يجب عليهم تزويد البرنامج بمزيد من الرياضيات لكي ترفع من كفاءة البرنامج.
أنشأ علماء الرياضيات مكتبة في عام 2017، وأطلقوا عليها اسم “mathlib”، وبدأوا بتزويدها بالمعرفة الرياضية العالمية، مما يجعلها نوعًا من أنواع مكتبة الإسكندرية في القرن الحادي والعشرين. كما ابتكر علماء الرياضيات وحمَّلوا أجزاء من الرياضيات الرقمية، وقاموا تدريجيًا ببناء كتالوج ليعتمد عليه برنامج (لين).
بناءً على كل ما سبق، فإن من المهم جدًا الاهتمام بالرياضيات -باعتبارها جزءًا أساسيًا في حياتنا- وتطويرها بشكل مستمر، نظرًا لأن الفترة التي نعيشها الآن هي فترة عصر الرقمنة.
كتابة: عبدالرحمن عادل
مراجعة: شيماء وصفي
تحرير: زياد محمد
