حلّها الحاسوب: مسائل رياضية شهيرة ساعدت الآلات في حلها (1976–2026)

في عام 1976 أعلن عالما رياضيات في إلينوي أنهما أثبتا أن أربعة ألوان تكفي لتلوين أي خريطة، وأن جزءًا من برهانهما لا يمكن التحقق منه إلا بالحاسوب. شعر كثير من علماء الرياضيات بقلق عميق: هل هو برهان حقًا إذا لم يستطع أي إنسان قراءته كاملًا؟ بعد خمسين عامًا انقلب السؤال. ففي 2026 وجدت أنظمة ذكاء اصطناعي الأفكار المفتاحية وراء نتائج عجز الخبراء عن إيجادها لعقود. يروي هذا المقال القصة بالترتيب، ويقول لكل مسألة شهيرة ما الذي فعلته الآلة بالضبط، لأن عبارة «حلّها الحاسوب» قد تعني أشياء مختلفة جدًا.

1976: أربعة ألوان، وبرهان لا يستطيع أحد قراءته

أساسيات GCSE

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

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

كيف زال الشك: تبع ذلك عام 1996 برهان حاسوبي أقصر، وفي 2005 تحقق جورج غونتييه وبنجامان فيرنيه من الحجة كاملة داخل مساعد البراهين Coq. واليوم تُعد من أكثر المبرهنات في الرياضيات خضوعًا للتحقق الدقيق.

1996: أول برهان وجده الحاسوب بنفسه

تعمّق جامعي

سألت حدسية روبنز هل تصف ثلاث قواعد قصيرة الجبر نفسه تمامًا الذي يصفه جبر بول، أي منطق الصواب والخطأ داخل كل شريحة حاسوب. عجز كبار المناطقة، ومنهم ألفريد تارسكي، عن حسمها ستين عامًا. وفي 1996 بحث المبرهن الآلي EQP الذي طوّره ويليام ماكيون في سلاسل الاستدلال الممكنة نحو ثمانية أيام، فوجد برهانًا. كان هذا مختلفًا في نوعه عن 1976: لم يخبر أحدٌ الحاسوب كيف ينبغي أن تبدو الحجة.

1998–2014: برتقالات كبلر

في عام 1611 ادّعى يوهانس كبلر أن الطريقة التي يكدّس بها باعة الفاكهة البرتقال (كل طبقة في تجاويف الطبقة التي تحتها) هي أكثف تعبئة ممكنة لكرات متساوية. وهي تملأ نحو 74% من الفراغ (بالضبط ⁦π/√18⁩).

حوّل توماس هيلز، مع صامويل فيرغسون، السؤال إلى آلاف مسائل التحسين وحلّها بالحاسوب، وأعلن برهانًا عام 1998. قال محكمو المجلة إنهم «متأكدون بنسبة 99%» من صحته، لكنهم لم يستطيعوا التحقق من كل حساب. فردّ هيلز بقيادة مشروع Flyspeck لإعادة التحقق من كل شيء ببرمجيات مساعد البراهين، واكتمل المشروع عام 2014.

2016: البرهان الذي حجمه 200 تيرابايت

أساسيات GCSE

إليك لغزًا يمكنك تجربته. لوّن كل عدد صحيح بالأحمر أو الأزرق. هل تستطيع ذلك بحيث لا تكون أي ثلاثية فيثاغورية (ثلاثة أعداد تحقق ⁦a² + b² = c²⁩، مثل 3 و4 و5) بلون واحد؟

عرض رونالد غراهام 100 دولار للإجابة. وفي 2016 شغّل ماراين هويله وأوليفر كولمان وفيكتور ماريك حلّال SAT (برنامجًا يحل ألغازًا منطقية ضخمة من نوع صواب/خطأ) على الحاسوب الفائق Stampede نحو يومين. والجواب: يمكن تلوين كل عدد من 1 إلى 7,824 بأمان، لكن لا يمكن ذلك من 1 إلى 7,825. وبلغ حجم البرهان على أنه لا يصلح أي تلوين لـ 7,825 عددًا 200 تيرابايت، ووصفته مجلة Nature حينها بأنه أكبر برهان رياضي على الإطلاق. وحسمت التقنية نفسها عام 2019 حدسية كيلر عن تبليط الفراغ بالمكعبات في سبعة أبعاد.

2025–2026: الذكاء الاصطناعي يبدأ بإيجاد الأفكار

تعمّق الدراسات العليا

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

حدسية مسافة الوحدة (مايو 2026). في عام 1946 سأل بول إردوش: إذا وضعت n نقطة على سطح مستوٍ، فكم زوجًا منها يمكن أن يكون على بُعد وحدة واحدة بالضبط؟ كان يعتقد أن الجواب ينمو أسرع قليلًا فقط من n. ووجد نموذج داخلي لدى OpenAI عائلة لا نهائية من مجموعات النقاط تتجاوز ذلك بقوة حقيقية من n، مستخدمًا أدوات عميقة من نظرية الأعداد الجبرية. تحقق منها تسعة من كبار علماء الرياضيات، منهم الحائزان على ميدالية فيلدز تيموثي غاورز وجاكوب تسيمرمان، وكتبوا ورقة مرافقة، وجعل ويل ساوين المكسب صريحًا. وشبّه جيل كالاي أهميتها ببرهان الألوان الأربعة عام 1976.

AlphaProof Nexus (مايو 2026). أطلقت Google DeepMind وكيلها الذي يجمع نموذج Gemini مع Lean على 353 مسألة مفتوحة من قاعدة بيانات مسائل إردوش. فحلّ 9 منها، بينها اثنتان ظلتا مفتوحتين 56 عامًا، وأثبت 44 حدسية من الموسوعة الإلكترونية للمتتاليات الصحيحة ⁦(OEIS)⁩. وكل برهان يُترجَم بنجاح في Lean. لكن لاحظ نسبة النجاح: نحو 2.5%.

Astra (أغسطس 2026). أعلنت OpenAI عشر نتائج من نموذجها التالي غير المنشور، منها أول بناء لـ زمرة غير سوفية (إجابة عن سؤال طرحه ميخائيل غروموف عام 1999)، وثلاث مسائل لإردوش، وأول تحسين منذ 1978 لحد عام في تعبئة الكرات. وكانت كل نتيجة مصحوبة بشهادة Lean. ولم يجد تدقيق بشري مستقل أخطاء جوهرية مؤكدة في النتائج الرئيسية، وإن طلب متخصص مراجعة كبيرة لإحداها، ولم تكن مراجعة المجلات العلمية قد اكتملت وقت الكتابة.

خمسون عامًا في خط زمني واحد

ماذا يعني هذا إن كنت تتعلم الرياضيات

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