التحقق من صحة برهان رياضي كبير قد يستغرق سنوات من المراجعة البشرية. لهذا السبب بالتحديد، أعلنت أنثروبيك أن Claude أنجز الشهر الماضي أول برهان صوري (Formal Proof) كامل لمبرهنة فيرما الأخيرة — واحدة من أشهر المبرهنات في تاريخ الرياضيات، وفي مشروع كان الخبراء يتوقعون له سنوات طويلة من العمل.
ماذا فعل Claude تحديدًا؟
البرهان الأصلي لمبرهنة فيرما وضعه السير أندرو وايلز عام 1995، بعد أكثر من 350 عامًا من طرح المسألة لأول مرة. ما فعله Claude مختلف: حوّل هذا البرهان إلى صيغة يمكن لأداة التحقق الآلي Lean أن تتحقق منها رياضيًا، سطرًا بسطر. النتيجة تجاوزت 13 مليون سطر من الكود، لتصبح أضخم برهان Lean يُكتب على الإطلاق. والأهم أن هذا العمل لم يكتفِ بإثبات المبرهنة نفسها، بل أثبت في الطريق أكثر من 29 ألف مبرهنة فرعية أخرى في مجالات رياضية متعددة لم تكن قد صيغت صوريًا من قبل.
لماذا يهمّك هذا حتى لو لم تكن مختصًا بالرياضيات؟
المسألة هنا أكبر من نتيجة تقنية واحدة. عدد الأبحاث والبراهين الرياضية التي تُنشر اليوم يفوق قدرة المجتمع العلمي على مراجعتها والتحقق منها بالسرعة نفسها. التحقق الآلي المدعوم بالذكاء الاصطناعي يفتح احتمالًا واقعيًا لتخفيف هذا العبء عن المراجعين البشر، دون أن يُلغي دورهم. وهذا العمل، كما وصفته أنثروبيك، يقوم على إرث ثلاثة قرون من الرياضيين ومئات المساهمين في مكتبة Mathlib المفتوحة — أي أنه ثمرة تراكم معرفي طويل، لا قفزة معزولة.
---
المصدر: حساب Anthropic الرسمي على منصة X، وتفاصيل إضافية على مدونة العلوم الخاصة بها: anthropic.com/research/formalizing-fermats-last-theorem
الكلمات المفتاحية: Claude، أنثروبيك، مبرهنة فيرما الأخيرة، البرهان الصوري، Lean، Mathlib، التحقق الآلي
No comments yet