التحقق الرسمي لإثبات الجبر الخطي باستخدام Lean

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