دليل غير قابل للمسح

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

جادل تيموتشكو بأن ثلاثة معايير تحدد ما إذا كانت الحجة برهانًا رياضيًا أم لا:

• الإقناع ، والذي يشير إلى قدرة البرهان على إقناع المُثبت العقلاني بنتيجته؛
• إمكانية التحقق ، والتي تشير إلى إمكانية وصول أعضاء المجتمع الرياضي البشري إلى البرهان للتحقق منه؛ و
• إمكانية الصياغة الرسمية ، والتي تشير إلى اعتماد البرهان فقط على العلاقات المنطقية بين المفاهيم لإثبات حجته. ^{[ 1 ]}

من وجهة نظر تيموتشكو، فشل برهان أبيل-هاكن في استيفاء معيار قابلية المسح، وذلك، كما جادل، باستبدال التجربة بالاستنتاج :

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

بدون إمكانية المسح، قد يحقق البرهان غرضه الأول المتمثل في إقناع القارئ بنتيجته، ولكنه قد يفشل في غرضه الثاني المتمثل في توضيح سبب صحة تلك النتيجة للقارئ - فقد يلعب دور الملاحظة بدلاً من دور الحجة. ^{[ 2 ] [ 3 ]}

هذا التمييز مهم لأنه يعني أن البراهين غير القابلة للمسح تُعرّض الرياضيات لاحتمالية خطأ أكبر بكثير. خاصةً في حالة عدم إمكانية المسح بسبب استخدام برنامج حاسوبي (قد يحتوي على أخطاء )، وبالأخص عندما يكون هذا البرنامج غير منشور، فقد تتأثر المصداقية نتيجةً لذلك. ^{[ 3 ]} كما كتب تيموتشكو:

لنفترض أن حاسوبًا فائقًا كُلِّف بدراسة اتساق حساب بيانو ، فأبلغ عن برهانٍ على عدم الاتساق ، برهانٌ طويلٌ ومعقدٌ لدرجة أن أي عالم رياضيات لم يستطع فهمه إلا في أبسط معانيه. هل يمكننا أن نثق بالحواسيب ثقةً كافيةً لقبول هذه النتيجة، أم سنقول إن الأدلة التجريبية على موثوقيتها غير كافية؟

إلا أن وجهة نظر تيموتشكو محل خلاف من خلال حجج مفادها أن البراهين التي يصعب مسحها ليست بالضرورة غير صالحة مثل البراهين التي يستحيل مسحها.

زعم بول تيلر أن سهولة الاستقصاء مسألة نسبية وتعتمد على القارئ، وليست سمة موجودة أو غير موجودة في البرهان. وكما لا تُرفض البراهين عندما يجد الطلاب صعوبة في فهمها، يجادل تيلر بأنه لا ينبغي رفضها (مع أنها قد تُنتقد) لمجرد أن علماء الرياضيات المحترفين يجدون صعوبة في متابعة الحجة. ^{[ 4 ] [ 3 ]} (خالف تيلر تقييم تيموتشكو القائل بأن "[نظرية الألوان الأربعة] لم يتم التحقق منها من قبل علماء الرياضيات، خطوة بخطوة، كما تم التحقق من جميع البراهين الأخرى. في الواقع، لا يمكن التحقق منها بهذه الطريقة.").

ومن الحجج المشابهة أن تقسيم الحالات هو أسلوب إثبات مقبول، وأن برهان أبيل-هاكن ليس إلا مثالاً متطرفاً على تقسيم الحالات. ^{[ 2 ]}

من جهة أخرى، فإنّ رأي تيموتشكو بأنّ البراهين يجب أن تكون قابلة للمراجعة على الأقل، وأنّ الأخطاء في البراهين التي يصعب مراجعتها أقل عرضةً للتدقيق، لا يُعارض عمومًا؛ بل اقتُرحت طرق لتحسين إمكانية المراجعة، لا سيما البراهين المُساعدة بالحاسوب. ومن بين الاقتراحات المبكرة التوازي: حيث يمكن تقسيم مهمة التحقق على العديد من المراجعين، بحيث يستطيع كلٌّ منهم مراجعة جزء من البرهان. ^{[ 5 ]} لكن الممارسة الحديثة، كما اشتهر بها فلايسبيك ، هي صياغة الأجزاء المشكوك فيها من البرهان في شكلٍ رسمي مُقيّد، ثم التحقق منها باستخدام مُدقّق براهين مُتاح للمراجعة. وبالفعل، فقد تم التحقق من برهان أبيل-هاكن بهذه الطريقة. ^{[ 6 ]}

ومع ذلك، لم يشهد التحقق الآلي انتشاراً واسعاً حتى الآن. ^{[ 7 ]}