Proof Assistants at the interplay of mathematical cultures: a semiotic-cultural analysis of proof in higher education
تستخدم هذه الورقة إطاراً سيميائياً-ثقافياً لتحليل كيفية عمل المساعدات الإثباتية، وتحديداً "Verbose Lean"، ككاشفات معرفية في الرياضيات الجامعية من خلال إعادة تشكيل ممارسات الإثبات وجعل الافتراضات الضمنية صريحة عبر الصياغة الرسمية الضرورية للكائنات الرياضية والخطوات الاستدلالية.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
في عالم الرياضيات الجامعية، يعد فعل إثبات قضية ما أكثر من مجرد حل مسألة؛ إنه ممارسة ثقافية. إنه طريقة محددة في التفكير والكتابة والتحقق من الأفكار، والتي يجب على الطلاب تعلمها مع انتقالهم من المدرسة الثانوية إلى التعليم العالي. لعقود من الزمن، راقب التربويون الطلاب وهم يكافحون لسد الفجوة بين الحجج الحدسية غير الرسمية التي تعلموها سابقاً، والمعايير الصارمة والصريحة المطلوبة في المستوى الجامعي. ومؤخراً، دخلت أداة جديدة هذا المشهد: "مساعد الإثبات" (proof assistant). هذه برامج حاسوبية مصممة للتحقق من الحجج الرياضية بدقة مطلقة، مما يجبر الكاتب على عدم ترك أي خطوة دون تفسير. وبينما يرى البعض هذه الأدوات وسيلة لجعل الرياضيات أكثر صرامة، يخشى آخرون أنها قد تقيد الإبداع أو تربك الطلاب الذين يعانون بالفعل. والسؤال ليس ببساطة ما إذا كانت هذه البرامج تساعد أم تعيق، بل كيف تغير الطبيعة الجوهرية لكيفية كتابة البرهان وفهمه.
قرر فريق من الباحثين في جامعتين فرنسيتين النظر عن كثب في هذا التفاعل. لم يكتفوا بالسؤال عما إذا كان الطلاب يتعلمون بشكل أفضل، بل راقبوا كيف أعاد البرنامج الحاسوبي تشكيل عملية تفكير الطلاب. ركزت الدراسة على مساق في السنة الأولى حيث استخدم الطلاب نوعاً معيناً من مساعدي الإثبات يسمى "Verbose Lean". وخلافاً للغات البرمجة القياسية التي تبدو كأنها أكواد برمجية، يسمح "Verbose Lean" للطلاب بالكتابة بلغة طبيعية منضبطة، مما يجعلها تبدو أقرب إلى الطريقة التي يتحدث بها الرياضيون ويكتبون بها على الورق. راقب الباحثون زوجاً من الطلاب يعملون على مسألة كلاسيكية: إثبات أنه إذا اقتربت متتالية من الأرقام أكثر فأكثر من قيمة موجبة، فإن الأرقام في تلك المتتالية يجب أن تصبح موجبة في نهاية المطاف. ومن خلال تسجيل محادثات الطلاب، وخربشاتهم على الورق، ونقراتهم على الشاشة، وردود فعل الكمبيوتر، رسم الباحثون خريطة مفصلة لكيفية انتقال الفكرة الرياضية من فكرة خام إلى حقيقة تم التحقق منها حاسوبياً.
ما وجده الباحثون هو أن الكمبيوتر لم يكتفِ بالتحقق من الإجابة النهائية فحسب، بل عمل كمرآة، كاشفاً عن الافتراضات الخفية التي عادة ما يتجاهلها الطلاب. في فصل دراسي عادي، قد يتخطى الطالب التفاصيل الصغيرة أو يعتمد على "شعور" بأن خطوة ما بديهية. ومع ذلك، فإن الكمبيوتر يتطلب تسمية وتبرير كل كائن، وكل شرط، وكل قفزة منطقية بشكل صريح. أظهرت الدراسة أن هذا المتطلب يفرض نوعاً من التحول الثقافي؛ فقد توجب على الطلاب ترجمة أفكارهم الانسيابية والحدسية إلى هيكل صارم يمكن للآلة فهمه. لم تكن هذه العملية سلسة، بل تضمنت ذهاباً وإياباً مستمراً بين ملاحظات الطلاب الورقية، وكلماتهم المنطوقة، ورسائل الخطأ من الكمبيوتر، وشروحات المعلم.
تتبع الباحثون تعبيراً رياضياً محدداً ظهر طوال عمل الطلاب. في البداية، تعامل الطلاب مع هذا التعبير كعدد مفيد للاستعانة به في استدلالهم. ومع ذلك، عندما حاولوا كتابته في الكمبيوتر، رفضه البرنامج. لم يقل الكمبيوتر إن العدد خاطئ رياضياً، بل قال إن العدد في المكان الخاطئ. لقد حاول الطلاب استخدامه كعلامة لموقع في متتالية، لكن الكمبيوتر احتاج إلى عدد صحيح لهذا الدور، بينما كان تعبيرهم عبارة عن كسر. كانت هذه اللحظة نقطة تحول؛ فقد أجبرت الطلاب على إدراك أنه في عالم مساعد الإثبات، فإن الدور الذي يلعبه العدد لا يقل أهمية عن العدد نفسه. توجب عليهم إعادة التفكير في استراتيجيتهم، ونقل التعبير من جزء في حجتهم إلى جزء آخر، حيث يتناسب أخيراً مع قواعد الكمبيوتر الصارمة.
لم تُحل هذه المعاناة بواسطة الكمبيوتر وحده. فالمعلم، الذي كان يعمل عند السبورة في نفس الفصل الدراسي، رسم رسماً بيانياً لشرح المفهوم بصرياً. وصف "نافذة" بحجم معين ساعدت الطلاب على رؤية لماذا يجب أن يكون عددهم أصغر من القيمة المستهدفة. هذا الشرح البصري، مقترناً برفض الكمبيوتر لمحاولتهم الأولى، ساعد الطلاب على إعادة تنظيم أفكارهم. أدركوا في النهاية أن العدد الذي كانوا يصارعونه لم يكن موقعاً في المتتالية، بل كان حجم الفجوة التي يحتاجون إلى قياسها. وبمجرد إجراء هذا التغيير، قبل الكمبيوتر حجتهم. لم يكن البرهان النهائي خطاً مستقيماً من الفكرة إلى الحل، بل كان رحلة معقدة حيث تغير معنى رمز واحد اعتماداً على ما إذا كان يُنطق به، أو يُكتب على الورق، أو يُشرح من قبل معلم، أو يتم فحصه بواسطة آلة.
تشير الدراسة إلى أن مساعدي الإثبات يعملون كـ "كاشفات معرفية" (epistemic revelators)، وهو المصطلح الذي يستخدمه المؤلفون لوصف الأدوات التي تجعل غير المرئي مرئياً. إنها تكشف عن "المسكوت عنه" في الرياضيات—الأجزاء من البرهان التي عادة ما يتركها الخبراء والطلاب دون ذكر لأنها تبدو بديهية. في الفصل الدراسي التقليدي، قد تمر هذه الفجوات دون ملاحظة، أما في فصل دراسي يحتوي على مساعد إثبات، فإن الكمبيوتر يجبر الطالب على ملء كل فجوة، كاشفاً عن القواعد الخفية التي تحكم الصحة الرياضية. ويرى الباحثون أن هذا لا يعني أن الكمبيوتر أفضل من الإنسان، أو أن الإنسان أفضل من الكمبيوتر، بل إن النظامين يعملان معاً لخلق مساحة جديدة حيث تتصادم وتندمج طرق مختلفة من التفكير في البرهان.
تشير النتائج إلى أن إدخال هذه الأدوات يغير ثقافة البرهان في التعليم العالي. الأمر لا يتعلق فقط بإضافة طبقة من الدقة التقنية، بل بإعادة تشكيل كيفية فهم الطلاب لما يعنيه أن يكون المرء على صواب. تظهر الدراسة أن الطلاب لا يتعلمون ببساطة كتابة الأكواد، بل يتعلمون التنقل بين عوالم مختلفة من المعنى. يجب عليهم تعلم ترجمة فهمهم الحدسي إلى لغة يمكن للآلة التحقق منها، مع الاستماع أيضاً إلى الشرح البشري للمعلم. رسائل الخطأ من الكمبيوتر ليست مجرد عقبات، بل هي إشارات تخبر الطالب بمكان نقص فهمه. ومن خلال إجبارهم على جعل افتراضاتهم الضمنية صريحة، توفر هذه الأدوات فرصة فريدة لدراسة كيفية بناء المعرفة الرياضية والتحقق من صحتها.
في الختام، تخلص الورقة البحثية إلى أن مساعدي الإثبات ليست أدوات محايدة؛ فهي تحمل معها أفكاراً محددة حول ما يعتبر حجة صالحة. عندما يستخدم الطلاب هذه الأدوات، فهم لا يتعلمون الرياضيات فحسب، بل يتعلمون مجموعة جديدة من القواعد الثقافية لكيفية التفكير والتواصل. ويقترح الباحثون أن هذا التحول يوفر مكاناً متميزاً لدراسة الاستمرارية والانقطاعات بين الطريقة التي يُدرس بها البرهان، والطريقة التي يمارسه بها الخبراء، والطريقة التي يتم بها التحقق من قبل الآلات. إن رحلة الطلاب في هذه الدراسة، من ارتباكهم الأولي إلى نجاحهم النهائي، توضح أن تعلم البرهان باستخدام الكمبيوتر هو عملية ترجمة؛ إنها عملية يتم فيها اختبار المعنى الرياضي، وإعادة تشكيله، وفي النهاية تثبيته من خلال التفاعل بين الحدس البشري، وتوجيه المعلم، ودقة الآلة.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.