تنص مبرهنة فيرما الأخيرة على أن xⁿ + yⁿ = zⁿ ليس لها حلول في الأعداد الصحيحة الموجبة حين تكون n أكبر من 2. خطّها بيير دو فيرما في هامش كتاب في ثلاثينيات القرن السابع عشر، وبرهنها أندرو وايلز في التسعينيات بشيء من أصعب الرياضيات التي كُتبت. وفي 4 سبتمبر 2026 أعلنت Anthropic أن Claude أنتج في 11 يومًا أول نسخة كاملة يتحقق منها الحاسوب من ذلك البرهان[1]. يشرح هذا المقال ما يعنيه ذلك، ولماذا هي قصة في علوم الحاسوب بقدر ما هي في الرياضيات، وما الذي لا تعنيه.
الجدول الزمني
- ثلاثينيات القرن 17يدّعي فيرما برهانًا «يضيق هذا الهامش عن احتوائه».
- 1994–95يكمل أندرو وايلز (مع ريتشارد تايلور) البرهان.
- 2024يبدأ كيفن بازارد في إمبريال كوليدج لندن مشروعًا بشريًا لصياغة البرهان رسميًا في Lean.
- أغسطس 2026يكمل وكلاء Claude صياغة رسمية كاملة في Lean خلال 11 يومًا.
- 4 سبتمبر 2026تعلن Anthropic النتيجة، ويراجعها بازارد.
ماذا يفعل مساعد البرهان
أساسيات GCSE
البرهان الذي يكتبه إنسان يترك خطوات صغيرة للقارئ. وحتى المحكّمون الخبراء قد تفوتهم ثغرة. ومساعد البرهان مثل Lean يزيل هذا الخطر. تكتب التعريفات والبراهين على شكل شيفرة، فيؤكد مدقّق صغير موثوق (النواة) أن كل خطوة تنتج عن المنطق وعن النتائج السابقة. فإذا تُرجمت الشيفرة، كانت المبرهنة متحققًا منها. إنه كمترجم برمجي يرفض تشغيل برنامجك ما لم يثبت أنه صحيح.
البرهان الرسمي شجرة: تستند المبرهنة النهائية إلى نتائج وسيطة كبرى، تستند بدورها إلى تمهيديات، تستند إلى تعريفات وحقائق أساسية. ويتحقق Lean من كل رابط. اضغط الزر لتتحقق من الشجرة بدءًا من الأساسات. مخطط توضيحي؛ الشجرة الحقيقية فيها نحو 29,500 مبرهنة.
ما الذي فعله Claude فعلًا
تعمّق A-Level
- صاغ رسميًا نسخة مبسّطة من برهان وايلز تعود إلى دارمون ودايموند وتايلور[1].
- النتيجة نحو 13 مليون سطر من Lean ونحو 30,300 مبرهنة (استُخدم نحو 29,500 منها في البرهان النهائي)، أي أكبر من خمسة أضعاف Mathlib[1].
- عمل عشرات من وكلاء Claude بالتوازي على مدى 11 يومًا، مستخدمين نحو ستة مليارات رمز مُخرَج من نموذج بحثي داخلي[1].
- اقتصرت المساهمة الرياضية البشرية على تعليمات عامة عرضية من باحث Anthropic تيانيي بنغ[1].
- لا يعتمد البرهان إلا على مسلّمات Lean القياسية الثلاث، وأكدت أداة مقارنة أن المبرهنة النهائية تنص تمامًا على ما تنص عليه صياغة Mathlib نفسها لمبرهنة فيرما الأخيرة[1].
- أعاد استخدام أجزاء من مشروع FLT لكيفن بازارد في إمبريال كوليدج لندن، وراجع بازارد البرهان المكتمل[1].
تحقّق سريع
ماذا يعني أن البرهان «يُترجَم» في Lean؟
لماذا يهم التحقق من نص المبرهنة
لا يفيد البرهان الذي يتحقق منه الحاسوب إلا إذا برهن النص الصحيح. فلو كُتبت المبرهنة في Lean خطأً ولو قليلًا، لكان البرهان الكامل للشيء الخطأ بلا قيمة. ولهذا استخدم الفريق أداة مقارنة لتأكيد أن النص يطابق الصيغة المكتوبة باستقلال في Mathlib، ولهذا يهم فحص «لا مسلّمات إضافية»: فهو يُظهر أن شيئًا لم يُفترض ببساطة[1]. والتحقق من الخطوات والمصادقة على المواصفة مهمتان منفصلتان، تمامًا كما في اختبار البرمجيات.
الفرق الذي يخلط بينه الطلاب غالباً
الصحيح ليس هو الأنيق (ولا الجديد).
سؤال بنمط الامتحان
اشرح الفرق بين التحقق (verification) والمصادقة (validation)، مستخدمًا البرهان الرسمي لمبرهنة فيرما الأخيرة مثالًا. [4 درجات]
إظهار الإجابة النموذجية وتوزيع الدرجات
- التحقق يفحص أن المنتج بُني بشكل صحيح، أي أنه يستوفي مواصفته (درجة واحدة)
- هنا يتحقق Lean من أن كل خطوة في البرهان صحيحة منطقيًا (درجة واحدة)
- المصادقة تفحص أن المنتج الصحيح هو الذي بُني، أي أن المواصفة تطابق ما كان مطلوبًا فعلًا (درجة واحدة)
- هنا تفحص مقارنة نص Lean بصياغة Mathlib المستقلة لـ FLT أن البرهان يبرهن المبرهنة المقصودة (درجة واحدة)
ما يركّز عليه الممتحن: عرّف المصطلحين واربط كلًا منهما بجزء محدد من المثال.
خطأ شائع: معاملة الكلمتين على أنهما مترادفتان. فقد يجتاز برنامج كل فحوص التحقق ويظل يفعل الشيء الخطأ.
المنطق والبرهان والاختبار تربط رياضيات A-Level بعلوم الحاسوب. ويقدّم مقالنا هل يستطيع الذكاء الاصطناعي حقًا حل الرياضيات؟ الصورة الأوسع، وتُظهر مسائل جائزة الألفية أي الأسئلة ما زالت مفتوحة.
المصادر ولمزيد من القراءة
- Anthropic: Formalizing Fermat's Last Theorem (4 Sep 2026) — الحجم، الوكلاء، المسلّمات، المساهمة البشرية، مراجعة بازارد، تحفظات
- AI Weekly: Claude formalized Fermat's Last Theorem in 11 days — تغطية إخبارية
- Lean community: Mathlib — مكتبة الرياضيات في Lean
- Imperial College London: Fermat's Last Theorem formalisation project (Kevin Buzzard) — المشروع الذي يقوده البشر
آخر مراجعة: 5 أكتوبر 2026. الأرقام قيم نموذجية منشورة، والقواعد قد تتغيّر. صياغة الامتحانات تختلف باختلاف المواصفة الدراسية، لذا تحقّق من مواصفتك أنت.
أسئلة شائعة
هل برهن الذكاء الاصطناعي مبرهنة فيرما الأخيرة؟
لا: برهنها أندرو وايلز في التسعينيات. ما حدث في 2026 هو أن وكلاء Claude ترجموا نسخة من ذلك البرهان إلى Lean، وهي لغة برمجة يتحقق مدقّقها من كل خطوة منطقية. والنتيجة التي أعلنتها Anthropic في 4 سبتمبر 2026 هي أول برهان كامل للمبرهنة يتحقق منه الحاسوب.
ما Lean؟
مساعد برهان: لغة برمجة تُكتب فيها التعريفات والمبرهنات والبراهين على شكل شيفرة. ويتحقق برنامج صغير موثوق، هو النواة، من أن كل خطوة تنتج عن قواعد المنطق والنتائج السابقة. فإذا تُرجم البرهان بنجاح، كانت المبرهنة متحققًا منها، بافتراض المسلّمات المضمّنة في Lean فقط.
ما حجم البرهان؟
نحو 13 مليون سطر من شيفرة Lean ونحو 30 ألف مبرهنة (استُخدم نحو 29,500 منها في البرهان النهائي)، أي أكبر من خمسة أضعاف Mathlib، مكتبة الرياضيات المجتمعية الرئيسية في Lean. واستغرق 11 يومًا، مع عشرات من وكلاء Claude يعملون بالتوازي وتوجيه عام عرضي من باحث Anthropic تيانيي بنغ.
هل البرهان الذي كتبه الذكاء الاصطناعي جيد؟
إنه صحيح بمعنى أن Lean تحقق منه، وقد راجعه كيفن بازارد الذي يقود مشروع الصياغة الرسمية البشري لـ FLT في إمبريال كوليدج لندن. لكن Anthropic تقول إنه على الأرجح أطول بكثير مما يلزم، وإن المحاولات الفاشلة تركت نحو 7% من أسطره غير القالبية. والصحيح ليس هو الأنيق.
تقييمات وآراء القراء
قيّم هذا المقال في عدة جوانب مختلفة — تقييمك يساعد القراء الآخرين، ويساعدنا على التحسّن.
هل كان هذا المقال مفيداً؟
أخبرنا برأيك — تصحيح، سؤال لم تتم الإجابة عنه، أو موضوع تودّ أن نغطيه لاحقاً.
تفضّل التحدث مباشرة؟ احجز مكالمة فيديو مجانية في الوقت الذي يناسبك: 15 دقيقة لسؤال سريع، و30 دقيقة لغير ذلك. تظهر المواعيد بتوقيتك المحلي.
عن الكاتب
Sudershan Soni
المؤسس والمدرّس الرئيسي في موستاك — مدرّس رياضيات وعلوم وعلوم حاسوب و STEM حاصل على الماجستير بخبرة تتجاوز 20 عاماً، يدرّس الطلاب من اختبار +11 و GCSE حتى A-Level وما بعده، عبر الإنترنت حول العالم.
اقرأ الملف الكامل