تعتبر “نظرية الألوان الأربعة” (Four Color Theorem) من أشهر النظريات في تاريخ الرياضيات، وفي الوقت نفسه أكثرها إثارة للجدل. فعلى الرغم من بساطة ادعائها لدرجة يمكن لطالب في المدرسة الابتدائية فهمه: “يكفي أربعة ألوان لتلوين أي خريطة مستوية بحيث تكون المناطق المتجاورة بألوان مختلفة”، إلا أن إثباتها استغرق أكثر من قرن من الزمان، وتطلب تحولاً جذرياً في النماذج الفكرية تمثل في “الإثبات بواسطة الحاسوب” والذي هز أساس علم الرياضيات.

في هذا المقال، سنقوم بتفكيك الصورة الكاملة لنظرية الألوان الأربعة بشكل شامل من منظور رياضي وتاريخي وفلسفي، بدءاً من السؤال البسيط في عام 1852، مروراً بتحديات وإخفاقات العباقرة، وصولاً إلى ذروة الرياضيات الحديثة التي اتخذت من الحاسوب كذكاء جديد حليفاً لها. وسنتعمق بشكل خاص في شرح مواضيع رياضية عميقة مثل الهيكل الهندسي لإثبات كيمب الخاطئ والمثال المضاد لهيوود، والإثبات الكامل لنظرية الألوان الخمسة، والرياضيات وراء طريقة التفريغ (Discharging Method)، وخوارزمية أبيل وهاكن، وتفاصيل الإثبات الشكلي باستخدام Coq، وعلاقة كل ذلك بمشكلة “NP-complete”.

الفصل الأول: عام 1852، سؤال فرانسيس غوثري البسيط والارتقاء نحو نظرية المخططات

طرح مسألة تلوين الخرائط

تعود بداية القصة إلى عام 1852، لشاب تخرج حديثاً من كلية لندن الجامعية في بريطانيا يُدعى فرانسيس غوثري. أثناء تلوينه لخريطة مقاطعات إنجلترا، لاحظ حقيقة غريبة: “مهما كانت الخريطة معقدة، ألا تكفي أربعة ألوان لتلوينها بحيث تكون المقاطعات المتجاورة بألوان مختلفة؟”

شارك فرانسيس هذا السؤال مع شقيقه فريدريك غوثري الذي كان يدرس الرياضيات في كلية لندن الجامعية آنذاك. قام فريدريك بعرض المسألة على أستاذه وعالم الرياضيات البارز أوغسطس دي مورغان. انجذب دي مورغان على الفور لجاذبية هذه المسألة، وشاركها عبر رسالة مع صديقه ويليام روان هاميلتون وآخرين. كانت تلك هي لحظة ولادة “مسألة الألوان الأربعة” التي تضيء تاريخ الرياضيات.

نظرية أويلر للمجسمات وثنائية المخططات المستوية

للتعامل مع مسألة تلوين الخرائط رياضياً وبشكل صارم، كان من الضروري صياغتها ضمن نظرية المخططات. إذا اعتبرنا كل منطقة على الخريطة (دولة أو مقاطعة) “رأساً” (Vertex)، وربطنا بين المناطق المتجاورة بـ “حافة” (Edge)، نحصل على “مخطط مستوٍ” (Planar Graph) لا تتقاطع حوافه على المستوى. تُعرف هذه العملية بأخذ “المخطط الثنائي” (Dual Graph). حيث تقابل حدود الخريطة الأصلية حواف المخطط، وتقابل المناطق رؤوسه.

وبذلك تُختزل مسألة الألوان الأربعة إلى “مسألة تلوين الرؤوس” (Vertex Coloring Problem) في المخطط: “هل يمكن تلوين رؤوس أي مخطط مستوٍ بأربعة ألوان بحيث يكون لأي رأسين متجاورين لونان مختلفان؟”.

يلعب اكتشاف ليونهارت أويلر لنظرية المجسمات دوراً بالغ الأهمية هنا. في المخطط المستوي المتصل، إذا كان عدد الرؤوس $V$، وعدد الحواف $E$، وعدد الأوجه $F$، فإن العلاقة الثابتة التالية تتحقق:

من خلال الجمع بين هذه النظرية والخصائص الأساسية للمخططات المستوية، يمكن استنتاج قيود قوية حول بنية المخططات المستوية. بافتراض أن المخطط بسيط لا يحتوي على حواف متعددة أو حلقات ذاتية، وباعتبار “المخطط المستوي الأعظمي” (Maximal Planar Graph) حيث تكون جميع الأوجه مثلثة. وبما أن إضافة حواف لأي مخطط مستوٍ لجعله أعظمياً لا يزيد من عدد الألوان اللازمة، يكفي إثبات نظرية الألوان الأربعة للمخططات المستوية الأعظمية.

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

بتعويض ذلك في صيغة أويلر لإلغاء $F$. نعوض $F = \frac{2}{3}E$ في $V - E + F = 2$:

في المخطط المستوي البسيط العام، نظراً لأن الأوجه محاطة بثلاث حواف أو أكثر، فإن $3F \leq 2E$، مما يؤدي إلى المتباينة التالية:

توضح هذه المتباينة أن هناك حداً أقصى صارماً لكثافة الحواف في المخطط المستوي. ومن هنا، دعونا نفكر في درجة كل رأس (Degree, $\deg(v)$). مجموع درجات جميع الرؤوس في المخطط يساوي ضعف عدد الحواف تماماً (تمهيدية المصافحة).

باستخدام المتباينة السابقة $2E \leq 6V - 12$:

بقسمة الطرفين على عدد الرؤوس $V$، نحصل على متوسط درجة الرأس:

حقيقة أن متوسط الدرجة أقل من 6 تماماً تثبت رياضياً وبشكل قاطع أن “رأساً واحداً على الأقل يجب أن تكون درجته 5 أو أقل”. بمعنى آخر، أي مخطط مستوٍ بسيط يحتوي على رأس واحد على الأقل بدرجة 1، 2، 3، 4، أو 5. هذه الحقيقة هي نقطة الانطلاق الأساسية لمفهوم “المجموعة الحتمية” الذي سنناقشه لاحقاً، وتمثل حجر الزاوية المطلق في إثبات نظرية الألوان الأربعة.

الفصل الثاني: “إثبات” ألفريد كيمب وانهياره بعد 11 عاماً

مفهوم سلسلة كيمب و “الإثبات” الرائع

في عام 1879، نشر المحامي وعالم الرياضيات البريطاني ألفريد براي كيمب (Alfred Kempe) أخيراً “إثباتاً” لمسألة الألوان الأربعة في مجلتي “Nature” و"American Journal of Mathematics". كان إثباته مبتكراً للغاية، وقبله مجتمع الرياضيات العالمي كإثبات صحيح لمدة 11 عاماً.

كان جوهر إثبات كيمب فكرة ثورية تُعرف اليوم باسم “سلسلة كيمب” (Kempe Chain). استخدم الاستقراء الرياضي، مفترضاً أن نظرية الألوان الأربعة صحيحة لجميع المخططات المستوية التي تحتوي على $k$ من الرؤوس، وحاول إثبات أنها صحيحة للمخططات التي تحتوي على $k+1$ من الرؤوس.

بناءً على نظرية أويلر المذكورة سابقاً، فإن المخطط المستوي $G$ ذي الرؤوس $k+1$ يحتوي دائماً على رأس $v$ بدرجة 5 أو أقل. لنفكر في المخطط $G'$ الناتج عن إزالة الرأس $v$ والحواف المتصلة به من المخطط $G$. نظراً لأن عدد رؤوس $G'$ هو $k$، فإنه يمكن تلوينه بـ 4 ألوان (لنقل الأحمر والأزرق والأخضر والأصفر) بناءً على فرضية الاستقراء. بعد ذلك، نعيد $v$ ونحاول تلوينه.

1. إذا كانت درجة $v$ هي 3 أو أقل: فإن الرؤوس المجاورة لـ $v$ هي 3 على الأكثر. وبالتالي، هناك لون واحد على الأقل من الألوان الأربعة غير مستخدم في الرؤوس المجاورة. بتلوين $v$ بهذا اللون غير المستخدم، يكتمل الإثبات.
2. إذا كانت درجة $v$ هي 4: لنفترض أن الرؤوس الأربعة المجاورة لـ $v$ (ولنسمها في اتجاه عقارب الساعة $v_1, v_2, v_3, v_4$) ملونة جميعها بألوان مختلفة (أحمر، أزرق، أخضر، أصفر). هنا، نفكر في مخطط جزئي مستخرج من المخطط الكلي يحتوي فقط على الرؤوس الملونة بـ “الأحمر” و"الأخضر" والحواف التي تربط بينها. إذا لم يكن $v_1$ (أحمر) و $v_3$ (أخضر) متصلين داخل هذا المخطط الجزئي الأحمر-الأخضر (أي لا يوجد مسار يمر عبر الرؤوس الحمراء والخضراء للانتقال من $v_1$ إلى $v_3$)، فيمكننا عكس ألوان المكون المتصل الذي يحتوي على $v_1$ (تغيير الأحمر إلى الأخضر والأخضر إلى الأحمر). وهذا ما يسمى “عكس سلسلة كيمب”. بعد العكس، يصبح $v_1$ أخضر، وتقل الألوان المحيطة إلى 3 ألوان: الأزرق والأخضر والأخضر والأصفر. وهذا يجعل من الممكن تلوين $v$ بالأحمر. وإذا كان $v_1$ و $v_3$ متصلين، فبسبب الخصائص الطوبولوجية للمخطط المستوي (نظرية منحنى جوردان المغلق)، فإن المسار الأحمر-الأخضر الذي يربط بين $v_1$ و $v_3$ سيفصل $v_2$ (أزرق) و $v_4$ (أصفر). وبالتالي، لا يمكن أبداً لـ $v_2$ و $v_4$ أن يتصلا في سلسلة كيمب زرقاء-صفراء، ويمكن عكس مكون الأزرق-الأصفر الذي يحتوي على $v_2$. في كلتا الحالتين، يمكن تقليل الألوان المحيطة بـ $v$ إلى 3 ألوان، ويمكن تلوين $v$.
3. إذا كانت درجة $v$ هي 5: نفكر في حالة تكون فيها الرؤوس الخمسة المحيطة بـ $v$ وهي $v_1, v_2, v_3, v_4, v_5$ ملونة على التوالي أحمر، أزرق، أخضر، أصفر، أحمر (نظراً لوجود 5 رؤوس، يجب أن يتكرر لون واحد). وسّع كيمب الحجة المستخدمة في الدرجة 4 وادعى أنه من خلال الدمج بمهارة بين عكس سلسلتي كيمب مختلفتين (على سبيل المثال، سلسلة حمراء-خضراء وسلسلة حمراء-صفراء)، يمكن دائماً تقليل الألوان المحيطة بـ $v$ إلى 3 ألوان أو أقل. طبّقت طريقته بشكل مزدوج المنطق القائل بأنه إذا كان أحدهما متصلاً، فإن الآخر مفصول.

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

مخطط هيوود المضاد: الخلل القاتل لـ “تقاطع سلاسل كيمب المزدوجة”

ولكن في عام 1890، قرأ عالم رياضيات يُدعى بيرسي جون هيوود (Percy John Heawood)، وكان يبلغ من العمر 29 عاماً آنذاك، ورقة كيمب بعناية فائقة، واكتشف قفزة منطقية قاتلة في الحجة المتعلقة بالرأس ذي الدرجة 5.

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

قام هيوود ببناء مخطط مضاد محدد (يُعرف اليوم باسم “مخطط هيوود المضاد” (Heawood graph) أو مشتقاته، وهو مخطط مستوٍ أعظمي مكون من 25 رأساً). في هذا المخطط، أظهر أنه عند تطبيق خوارزمية كيمب لتقليل الألوان المحيطة بالرأس $v$ ذي الدرجة 5، فبمجرد عكس السلسلة الزرقاء-الخضراء، تتصل السلسلة الزرقاء-الصفراء التي لم تكن متصلة في الأصل. وبعد ذلك، عند عكس السلسلة الزرقاء-الصفراء، تعود الرؤوس الخضراء التي تم عكسها للتو إلى ألوانها الأصلية، مما يؤدي إلى حلقة لا ينخفض فيها عدد الألوان.

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

الإثبات الرياضي الكامل لنظرية الألوان الخمسة

انهار إثبات كيمب، لكن هيوود لم يكتفِ بالهدم فقط. فقد أدرك أن فكرة كيمب نفسها (سلسلة كيمب) مفيدة للغاية، واستخدمها لتقديم إثبات صارم لـ “نظرية الألوان الخمسة” (Five Color Theorem) والتي تنص على أن “جميع المخططات المستوية يمكن تلوينها بالضرورة بـ 5 ألوان”. عملية الإثبات الكاملة لنظرية الألوان الخمسة هي كالتالي:

النظرية: أي مخطط مستوٍ $G$ قابل لتلوين الرؤوس بـ 5 ألوان. الإثبات: نستخدم الاستقراء الرياضي على عدد الرؤوس $n$. الحالة حيث $n \leq 5$ بديهية. نفترض أن جميع المخططات المستوية لـ $n=k$ يمكن تلوينها بـ 5 ألوان، ونفكر في المخطط المستوي $G$ لـ $n=k+1$. استناداً إلى الحقيقة المشتقة من صيغة أويلر، يحتوي $G$ دائماً على رأس $v$ درجته 5 أو أقل. بما أن المخطط $G' = G - \{v\}$ الناتج عن إزالة $v$ من $G$ يحتوي على $k$ من الرؤوس، فهو قابل للتلوين بـ 5 ألوان (لون 1، لون 2، لون 3، لون 4، لون 5) حسب فرضية الاستقراء. نفكر في إعادة الرأس $v$ مع الحفاظ على تلوين المخطط $G'$.

• الحالة 1: إذا كانت $\deg(v) < 5$. بما أن الرؤوس المجاورة لـ $v$ هي 4 على الأكثر، فهناك لون واحد على الأقل من الألوان الخمسة غير مستخدم في الرؤوس المجاورة. نلوّن $v$ بهذا اللون.
• الحالة 2: إذا كانت $\deg(v) = 5$. لنفترض أن الرؤوس الخمسة المجاورة لـ $v$ وهي $v_1, v_2, v_3, v_4, v_5$ (مرتبة في اتجاه عقارب الساعة) ملونة جميعها بألوان مختلفة (اللون 1، اللون 2، اللون 3، اللون 4، اللون 5 على التوالي). (إذا تم استخدام نفس اللون مرتين أو أكثر، سيتبقى لون واحد أو أكثر غير مستخدم يمكن تلوين $v$ به). هنا، في المخطط $G'$، نعتبر المخطط الجزئي المستحث المكون فقط من الرؤوس الملونة باللون 1 واللون 3، ولنسمِ المكون المتصل الذي يحتوي على $v_1$ فيه بـ $C_{13}$ (هذه هي سلسلة كيمب).
  • الحالة الفرعية 2a: إذا كان $v_3 \notin C_{13}$. بعبارة أخرى، لا يوجد مسار من $v_1$ إلى $v_3$ يمر فقط بالرؤوس ذات اللون 1 واللون 3. في هذه الحالة، حتى إذا قمنا بعكس ألوان جميع الرؤوس في $C_{13}$ (اللون 1 $\leftrightarrow$ اللون 3)، تظل صحة التلوين محفوظة. بعد العكس، يصبح لون $v_1$ هو اللون 3، وبما أن $v_3$ هو اللون 3 أيضاً، فلن يعود اللون 1 موجوداً في الرؤوس المحيطة بـ $v$. وبالتالي يمكن تلوين $v$ باللون 1.
  • الحالة الفرعية 2b: إذا كان $v_3 \in C_{13}$. بعبارة أخرى، يوجد مسار $P_{13}$ يربط بين $v_1$ و $v_3$ ومكون من الرؤوس ذات اللون 1 واللون 3. هذا المسار $P_{13}$ مع الرأس $v$ والحافتين $(v, v_1), (v, v_3)$ يشكلون منحنياً مغلقاً (دورة) على المستوى. بناءً على خصائص المخططات المستوية (نظرية منحنى جوردان المغلق)، تقسم هذه الدورة المستوى إلى قسمين: داخلي وخارجي. يقع الرأسان $v_2$ و $v_4$ في جانبين مختلفين من هذه الدورة (أحدهما في الداخل والآخر في الخارج). هنا، نفكر في سلسلة كيمب $C_{24}$ المكونة من الرؤوس الملونة باللون 2 واللون 4. إذا افترضنا أن $v_2$ و $v_4$ متصلان بهذه السلسلة، يجب أن يكون هناك مسار $P_{24}$ يربط بين $v_2$ و $v_4$. ومع ذلك، يجب أن يمتد $P_{24}$ على المخطط المستوي دون أي تقاطع، ولكنه لا يمكن أن يعبر الدورة التي شكلها $P_{13}$ (وهذا يتعارض مع تعريف المخطط المستوي). لذلك، لا يوجد مسار إطلاقاً يربط $v_2$ بـ $v_4$ ويتكون من اللون 2 واللون 4. أي أن سلسلة كيمب $C_{24}$ ذات اللونين 2-4 التي تحتوي على $v_2$ لا تحتوي على $v_4$. وبالتالي، بعكس الألوان في $C_{24}$ (اللون 2 $\leftrightarrow$ اللون 4)، سيصبح لون $v_2$ هو اللون 4، وسيختفي اللون 2 من حول $v$. وفي النهاية، يمكننا تلوين $v$ باللون 2.

بناءً على ما سبق، يمكن تلوين $v$ في جميع الحالات، وبذلك تم إثبات نظرية الألوان الخمسة بالكامل باستخدام الاستقراء الرياضي. $\blacksquare$

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

الفصل الثالث: الرياضيات وراء طريقة التفريغ (Discharging Method) واستنتاج التشكيلات الحتمية

بعد هيوود، بدأ علماء الرياضيات بافتراض وجود “أصغر مثال مضاد لا يمكن تلوينه بأربعة ألوان” (Minimum Counterexample)، وشرعوا في استكشاف الهيكل الذي يجب أن يتخذه (أو لا يجب أن يتخذه) عن طريق البرهان بالخلف. وهنا ظهرت أهمية مفهومين قويين هما: “التشكيلة القابلة للاختزال” (Reducible Configuration) و"المجموعة الحتمية" (Unavoidable Set).

القابلية للاختزال (Reducibility)

التشكيلة القابلة للاختزال تعني “نمطاً محلياً من الرؤوس يستحيل أن يوجد داخل المخطط إذا كان المخطط بالكامل لا يمكن تلوينه بأربعة ألوان (أي إذا كان أصغر مثال مضاد)”. على سبيل المثال، “الرأس ذو الدرجة 3 أو أقل” أو “الرأس ذو الدرجة 4” يعتبر تشكيلة قابلة للاختزال. لأنه وكما ذكرنا سابقاً، باستخدام الاختزال عن طريق سلسلة كيمب، إذا كانت هذه الرؤوس موجودة، فمن الممكن اختزال المسألة إلى مخطط أصغر، مما يتناقض مع افتراض أنه “أصغر مثال مضاد”. في عام 1913، أثبت جورج ديفيد بيركهوف (George David Birkhoff) أن تشكيلة معينة تتكون من 6 رؤوس تُعرف باسم “ماسة بيركهوف” هي أيضاً قابلة للاختزال. رغم توالي الاكتشافات للتشكيلات القابلة للاختزال، إلا أن الإثبات لن يكتمل دون ضمان أنها “موجودة حتماً” داخل المخطط.

الهيكل الرياضي لطريقة التفريغ (Discharging Method)

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

لصياغة هذه المجموعة الحتمية وإثباتها، تم استخدام سلاح قوي للغاية يُعرف باسم “طريقة التفريغ” (Discharging Method) والذي قام بصقله هاينريخ هيش (Heinrich Heesch). طريقة التفريغ هي تقنية شبه سحرية لإثبات النظريات الهيكلية في نظرية المخططات، وتستخدم مفهوم الشحنة الكهربائية من الكهرومغناطيسية كقياس.

العملية الرياضية لطريقة التفريغ هي كالتالي:

1. $$ch(v) = 6 - \deg(v)$$

   بناءً على المعادلة $\sum_{v} (6 - \deg(v)) = 12$ المستقاة من صيغة أويلر، فإن المجموع الكلي للشحنات الأولية للمخطط بأكمله يساوي تماماً 12 (قيمة موجبة). في هذه الحالة، يكون للرأس ذي الدرجة 5 شحنة $+1$، والرأس ذي الدرجة 6 شحنة $0$، والرؤوس ذات الدرجة 7 فأكثر تحمل شحنات سالبة. (نظراً لأننا يمكن أن نفترض أن أصغر مثال مضاد لا يحتوي على رؤوس بدرجة 4 أو أقل، نعتبر 5 هي الدرجة الدنيا).

2. تحديد قواعد نقل الشحنات (Discharging Rules): بعد ذلك، نحدد القواعد لنقل الشحنات بين الرؤوس المتجاورة. الفكرة الأساسية هي “تفريغ الشحنة من الرأس ذي الشحنة الموجبة (أي الرأس ذي الدرجة 5) إلى الرأس ذي الشحنة السالبة (الرؤوس عالية الدرجة كـ 7 فأكثر)”. على سبيل المثال، نضع العشرات أو المئات من القواعد التفصيلية مثل: “إذا كان الرأس $v$ ذو الدرجة 5 مجاوراً لرأس $u$ ذي الدرجة 7، يتم نقل شحنة بمقدار $\frac{1}{5}$ من $v$ إلى $u$”.

3. $$ \sum_{v \in V} ch'(v) = 12 > 0 $$

   ($ch'(v)$ تمثل شحنة الرأس $v$ بعد النقل) كون المجموع الكلي موجباً يعني أنه “حتى بعد نقل الشحنات، يجب أن يوجد رأس واحد على الأقل يحمل شحنة موجبة”.

   هنا، نقوم بتحليل الشحنة النهائية $ch'(v)$ لكل رأس بناءً على هيكله المحلي (نمط درجات الرأس نفسه والرؤوس المجاورة له). إذا تمكنا من إثبات أن “الرأس الذي لا يحتوي على تشكيلة محددة، وفقاً لقواعد التفريغ المحددة، ستكون شحنته النهائية دائماً صفراً أو أقل”، فلكي تكون الشحنة النهائية موجبة، يجب أن توجد هذه “التشكيلة المحددة” في مكان ما داخل المخطط. وبهذه الطريقة، فإن القائمة الشاملة لجميع أنماط التشكيلات المحلية التي تجعل الشحنة النهائية موجبة تصبح هي “المجموعة الحتمية”.

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

الفصل الرابع: عام 1976، خوارزمية التحقق الحاسوبي لأبيل وهاكن

تعريف D-reduction و C-reduction

في السبعينيات، شرع كينيث أبيل (Kenneth Appel) ووولفجانج هاكن (Wolfgang Haken) من جامعة إلينوي في مشروع تاريخي لدمج طريقة التفريغ لهيش مع القوة الحسابية للحواسيب.

كانت المهمة الأكثر تطلباً للحسابات التي واجهوها هي “تحديد قابلية الاختزال” للتشكيلات. هناك نوعان رئيسيان للقابلية للاختزال:

• الاختزال المباشر (D-reducibility / Direct reducibility): لجميع الأنماط الممكنة لتلوين الحدود الحلقية (Ring) المحيطة بالتشكيلة بـ 4 ألوان، ما إذا كان يمكن تمديد هذا التلوين إلى داخل التشكيلة، أو إذا كان من الممكن تحويله إلى نمط قابل للتمديد الداخلي عن طريق عكس سلسلة كيمب لألوان الحدود. إذا تم التأكد من ذلك، يمكن القول فوراً أن هذه التشكيلة غير موجودة في أصغر مثال مضاد.
• الاختزال الانكماشي (C-reducibility / Contracting reducibility): إذا كانت هناك أنماط تفشل في تحقيق الاختزال المباشر (D-reducibility)، نفكر في مخطط أصغر نتج عن “تقليص” (دمج عدة رؤوس في رأس واحد) جزء من التشكيلة، ونبين أنه إذا كان المخطط المقلص قابلاً للتلوين بـ 4 ألوان، فإن المخطط الأصلي قابل أيضاً للتلوين بـ 4 ألوان.

خوارزمية تحديد قابلية التلوين للحدود الحلقية

المهمة التي أوكلت إلى الحاسوب (IBM 360) هي تنفيذ خوارزمية تحديد الاختزالين (D و C) لعدد هائل من التشكيلات المرشحة.

لنفترض أن التشكيلة $C$ لها حدود حلقية $R$ (طولها $k$). عدد التوافيق الممكنة لتلوين الرؤوس على الحلقة بـ 4 ألوان هو $4^k$ كحد أقصى، وحتى مع مراعاة التماثل، يبقى العدد هائلاً. على سبيل المثال، إذا كان طول الحلقة $k=14$، فيلزم التحقق من صحة تلوين الحدود لحوالي 200 ألف نمط. تتقدم الخوارزمية حسب الخطوات التالية:

1. إنشاء مجموعة من جميع الأنماط الصالحة لتلوين الحدود الحلقية $R$ بـ 4 ألوان.
2. تجربة جميع الطرق الممكنة لتلوين الجزء الداخلي من التشكيلة $C$ بـ 4 ألوان فعلياً، وتسجيل الأنماط الحدودية التي تتوافق معها (الأنماط القابلة للتمديد داخلياً).
3. بالنسبة للأنماط الحدودية غير القابلة للتمديد الداخلي، نقوم بمحاكاة عكس سلسلة كيمب. إذا أدى العكس إلى الانتقال إلى نمط ثبت مسبقاً أنه “قابل للتمديد داخلياً”، يُعتبر النمط الأولي أيضاً “محلولاً”.
4. نكرر البحث عن هذا الانتقال العكسي، وإذا تم حل جميع الأنماط الحدودية، يتم اعتبار التشكيلة $C$ على أنها “D-reducible” (قابلة للاختزال المباشر).

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

1200 ساعة من الحسابات و “Q.E.D.” (وهو المطلوب إثباته)

في عام 1976، اكتشفا أخيراً مجموعة حتمية تتكون من 1,936 تشكيلة، مستمدة من قواعد التفريغ المبنية بعناية فائقة. وبعد تشغيل الحاسوب المركزي لجامعة إلينوي لأكثر من 1200 ساعة، أكد الحاسوب أن جميع التشكيلات البالغ عددها 1,936 هي إما قابلة للاختزال D أو C.

كتبا في ملخص بحثهما جملة قصيرة: “Every planar map is four colorable.” “كل خريطة مستوية قابلة للتلوين بأربعة ألوان.”

على ختم البريد الخاص بقسم الرياضيات بجامعة إلينوي، نُقشت عبارة تفخر بإنجازهم: “FOUR COLORS SUFFICE” (أربعة ألوان تكفي). كان هذا الحدث تذكارياً، حيث كانت المرة الأولى في تاريخ الرياضيات التي يتحمل فيها الحاسوب عبء خطوة استنتاجية مركزية في إثبات نظرية رياضية.

الفصل الخامس: الزلزال في مجتمع الرياضيات وفلسفة “الإثبات”

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

هل الإثبات الذي لا يستطيع الإنسان قراءته يُعتبر رياضيات؟

في التقليد الرياضي المستمر منذ اليونان القديمة، كان “الإثبات” يعني قيام عالم الرياضيات البشري بتتبع الخطوات المنطقية واحدة تلو الأخرى، وفهم صحتها والاقتناع بها من أعماق القلب. وكان يُعتقد أن عملية الإثبات تحمل في طياتها رؤية عميقة لـ “سبب صحة النظرية” وجمال البنية.

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

نشأ وضع غير مسبوق حيث “للاقتناع بصحة الإثبات، يجب أن نؤمن بأن أجهزة الحاسوب (الهاردوير) لم تتعطل، وأن البرنامج الذي كتبه أبيل وهاكن بلغة التجميع (Assembly language) خالٍ من الأخطاء”.

انتقد فيلسوف العلم توماس تيموتشكو (Thomas Tymoczko) هذا الإثبات، معتبراً أنه قد انحدر من السعي وراء الحقيقة القبلية (A priori) في الرياضيات البحتة إلى شيء يشبه العلوم التجريبية والتطبيقية مثل الفيزياء. تعرض تعريف فعل “الإثبات” نفسه لأزمة إبستمولوجية (معرفية).

الردود والتبسيط بواسطة RSST

رد أبيل وهاكن على هذه الانتقادات قائلين: “الرياضيات ليست مجرد براهين جميلة فقط. هناك مسائل معقدة بطبيعتها وتتطلب تقسيمات ضخمة للحالات، وإذا كانت تتجاوز قدرات الدماغ البشري، فإن الاستعانة بقوة الآلة يمثل تطوراً حتمياً”.

لتبديد هذا الغموض، حاول العديد من علماء الرياضيات تبسيط الإثبات وإعادة التحقق منه. في عام 1997، نشر أربعة باحثين هم نيل روبرتسون (Neil Robertson)، ودانيال ساندرز (Daniel P. Sanders)، وبول سيمور (Paul Seymour)، وروبن توماس (Robin Thomas) (يُعرفون باسم RSST) إثباتاً جديداً قاموا فيه بتحسين طريقة التفريغ لتصبح أكثر منهجية وأسهل للتحقق البشري، وتمكنوا من تقليص حجم المجموعة الحتمية من 1,936 تشكيلة إلى 633 تشكيلة. كانت هذه خوارزمية محسنة تنجز الحسابات في بضع ساعات.

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

الفصل السادس: الإثبات الشكلي الكامل لجورج غونتييه باستخدام Coq

كيف يمكن تبديد القلق المتمثل في “احتمالية وجود أخطاء (Bugs) في البرنامج” رياضياً وبشكل كامل؟ الإجابة النهائية لذلك هي “الصياغة الشكلية الكاملة” (Formalization) باستخدام “نظام المساعدة في إثبات النظريات” (Proof Assistant).

في عام 2005، نجح جورج غونتييه (Georges Gonthier) من المعهد الوطني لأبحاث الحوسبة والأتمتة في فرنسا (INRIA) ومايكروسوفت للأبحاث، بالتعاون مع بنجامين ويرنر (Benjamin Werner)، في صياغة الإثبات بشكل كامل وجذري لنظرية الألوان الأربعة باستخدام نظام “Coq” للمساعدة في الإثبات.

صياغة الخريطة الفائقة المحدودة (Hypermap) والطوبولوجيا التوافقية

يعد Coq نظاماً يصف ويتحقق آلياً من البراهين بناءً على نظام قواعد منطقية صارم للغاية (Calculus of Inductive Constructions: حساب البناء الاستقرائي) بدءاً من البديهيات الرياضية.

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

إثبات صحة برنامج الإثبات نفسه

علاوة على ذلك، تخلى غونتييه عن “برامج التحقق المكتوبة بلغة C” التي استخدمها أبيل-هاكن وRSST، وقام بتطبيق الخوارزمية نفسها التي تحدد القابلية للاختزال باستخدام لغة Coq الداخلية (Gallina). ثم قام بإثبات صحة الخوارزمية رياضياً داخل Coq، بحيث “إذا أنتجت الخوارزمية (True)، فإن التشكيلة قابلة للاختزال حقاً”.

وبهذا، تغيرت موثوقية الإثبات بشكل قاطع. لم تعد هناك حاجة للقلق من “أخطاء الخوارزميات”. والسبب هو أنه طالما أن النواة الأساسية للتحقق المنطقي في نظام Coq (والتي تتكون من بضع مئات من أسطر الأوامر البسيطة والصلبة والمُطبقة باستخدام مؤشرات دي بروين وغيرها) تعالج قواعد الاستدلال المنطقي بشكل صحيح، فإن شجرة الإثبات الضخمة التي بناها غونتييه مضمونة رياضياً لتكون صحيحة تماماً.

هذا يمثل إنجازاً جديداً لـ “الإثبات” في الرياضيات. إنه تطور من “الإثبات الذي يقرؤه الإنسان ويفهمه” (Informal Proof) إلى “الإثبات الشكلي الذي تضمن فيه الآلة الكمال المنطقي” (Formal Proof). أصبحت نظرية الألوان الأربعة أول نظرية كبرى غير بديهية في التاريخ تصل إلى هذا المستوى الأقصى من الصرامة.

الفصل السابع: مسألة الألوان الأربعة للمخطط المستوي ومفارقة NP-complete

أخيراً، لنلقِ نظرة على نظرية الألوان الأربعة من منظور نظرية التعقيد الحسابي (Computational Complexity Theory). هناك ظاهرة مثيرة للاهتمام تُشبه المفارقة هنا.

تُعتبر مسألة التلوين للمخططات العامة (مسألة تحديد ما إذا كان يمكن تلوين مخطط معطى بـ $k$ ألوان) من أشهر مسائل “NP-complete” في علوم الحاسوب. وعلى وجه الخصوص، تم إثبات أن مسألة “تلوين المخطط المستوي بـ 3 ألوان” (Planar 3-Colorability) هي مشكلة من نوع NP-complete. هذا يعني أنه، ما لم يكن $\text{P} = \text{NP}$، يُعتقد أنه لا توجد خوارزمية لحل هذه المسألة (تحديد إمكانية التلوين بـ 3 ألوان) في وقت كثير الحدود.

إذاً، ماذا عن “تلوين المخطط المستوي بـ 4 ألوان” (Planar 4-Colorability)؟ نظراً لأن 3 ألوان هي NP-complete، قد يوحي الحدس بأن 4 ألوان ستكون بنفس الصعوبة (أي NP-complete).

لكن من المثير للدهشة أن التعقيد الحسابي لمسألة تلوين المخطط المستوي بـ 4 ألوان (كمشكلة قرار) هو $O(1)$، أي في “وقت ثابت (بديهي)”. السبب هو أن نظرية الألوان الأربعة تضمن أن “جميع المخططات المستوية يمكن تلوينها بأربعة ألوان”. وبناءً عليه، يمكن للخوارزمية ببساطة إخراج “نعم” (Yes) دون حتى النظر إلى المخطط المُدخل وستكون الإجابة دائماً صحيحة بنسبة 100%. هذا مثال جميل على كيفية قدرة الضمان القوي للوجود الذي تقدمه النظرية على تقليص تعقيد مشكلة القرار إلى أدنى مستوى.

ومع ذلك، فإن هذا الحديث يقتصر فقط على مشكلة القرار (Decision Problem): “هل يمكن التلوين أم لا؟”. بناء خوارزمية تلوين تُحدد “كيف يمكن التلوين بـ 4 ألوان فعلياً” (Search Problem) هو أمر مختلف تماماً. عند تحويل إجراءات الإثبات لكل من أبيل-هاكن و RSST إلى خوارزميات، نحصل على خوارزمية قادرة على تحديد التلوين الفعلي بـ 4 ألوان لمخطط مستوٍ يحتوي على عدد $N$ من الرؤوس. تبين أن الخوارزمية المعتمدة على إثبات RSST تنتج التلوين بـ 4 ألوان في وقت كثير الحدود وبأسوأ حالة تعقيد $O(N^2)$.

بمعنى آخر، قد يستغرق تلوين المخطط المستوي بـ 3 ألوان وقتاً يُضاهي عُمر الكون (NP-complete)، ولكن بمجرد إضافة لون رابع، وبفضل البنية الرياضية العميقة لنظرية الألوان الأربعة، تصبح هناك خوارزمية سريعة (بزمن $O(N^2)$). هذه حقيقة ساحرة وغامضة للغاية تُبرز التلاقي بين الرياضيات وعلوم الحاسوب.

الخلاصة: ما تركته نظرية الألوان الأربعة

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

يمثل تاريخ نظرية الألوان الأربعة تقاطعاً حاداً بين حدود الحدس البشري وإمكانات محرك المنطق الجديد المتمثل في “الآلة”. في وقتنا الحاضر، تم إثبات معضلات رياضية ضخمة أخرى بشكل كامل باستخدام التحقق الشكلي في أنظمة المساعدة في الإثبات، مثل حدسية كيبلر (Kepler conjecture) (عام 2014، مشروع Flyspeck بواسطة توماس هيلز) ونظرية فايت-طومسون (Feit-Thompson theorem).

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