في عام 2016، حققت الرياضيات إنجازًا مذهلاً عندما نجحت العالمة فياوزوفسكا في حل معضلة تعبئة الكرات في البعد الثامن (Sphere Packing Problem in Dimension 8) باستخدام نماذج رياضية معقدة تُعرف بالأشكال المودولارية (Modular Forms). هذا الحل لم يكن مجرد إنجاز فردي، بل تصور إمكانية وجود وظيفة سحرية (Magic Function) تلبي شروطًا مثالية وضعها الباحثان كوهين وإلكيس في عام 2003.

ولكن القصة لم تنتهي هنا! ففي مارس 2024، انطلق الباحثان هاريهيران وفياوزوفسكا في مشروع طموح يهدف إلى توثيق هذا الحل والتفاصيل الرياضية المرتبطة به في برنامج ‘Lean Theorem Prover’.

وفي فبراير 2026، تم تحقيق مرحلة بارزة عندما تم التحقق بشكل رسمي من هذا الإنجاز، حيث ساهم نموذج التحقق الذاتي 'Gauss' التابع لشركة Math, Inc. في المراحل النهائية من التحقق.

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