- Lean أداة إثبات تستخدم آلة للتحقق من صحة البراهين الرياضية والبرامج. وبحسب هذا المقال، أُضيف أمر lake check إلى Lean v4.35.0، ويمكن بعده تصدير العمل وإعادة فحصه بالمدقق الرسمي leanchecker. تعمل العملية كاملة داخل بيئة معزولة (sandbox) افتراضيًا.
- عند استخدام الخيار lake check --paranoid يُعاد فحص العمل نفسه بأربعة مدققات إضافية هي nanoda وlean4lean و con-leche و con-ron. كما تعمل نسخة معززة الذاكرة من المدقق الرسمي، بحيث تظهر أخطاء الذاكرة كتوقف للفحص بدلًا من نتيجة خاطئة بصمت.
- يذكر المقال أن con-leche أول نواة مكتوبة بلغة Lean وأُثبت اتساقها. يعتمد الإثبات على نموذج من نظرية المجموعات، ويوصف النهج بأنه يقلل الأخطاء من نوع أخطاء التنفيذ. وفي التصدير الكامل لـ Mathlib، يذكر المؤلف قياسًا قدره 0.69 مرة من عدد التعليمات في النواة الرسمية، باستخدام 8 خيوط خلال نحو 100 ثانية.
- con-ron نواة نقلتها أداة ذكاء اصطناعي من con-leche إلى Rust، ثم أُثبت باستخدام أداة Aeneas أنها تطابق خوارزمية الفحص الأصلية. وAeneas أداة تتحقق من شيفرة Rust باستخدام Lean. ويشرح المقال أن استخدام النواتين معًا يوفر حماية أعلى من الأخطاء في مترجم Lean أو في بيئة تشغيله.
O: يفيد هذا الأمر الباحثين الذين يكتبون البراهين بلغة Lean ويرغبون في تشغيل lake check --paranoid على مشروعهم الخاص للتحقق من أن نتائج الأدوات الأربع الإضافية تطابق نتائج الأداة الرسمية.
X: إن عدد الأوامر مقارنةً بـ 0.69 وقيمة 100 ثانية المتعلقة بـ con-leche هي قياسات أعدّها المؤلفون، ولم تُكشف شروط القياس بالكامل، لذا ينبغي التحقق منها في بيئتك الخاصة.