Not Letting Proofs Die: xLaDe, a Lean 4 Ecosystem Framework

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

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

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

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

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

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

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