أعلنت شركة Leanstral عن إصدار نموذج Leanstral 1.5، وهو نموذج ذكاء اصطناعي مفتوح المصدر مخصص للتحقق الرسمي من البراهين الرياضية والأكواد البرمجية ضمن بيئة Lean 4. يحمل النموذج ترخيص Apache-2.0 ويتألف من 119 مليار معلمة إجمالية مع 6 مليارات معلمة نشطة، مما يوفر توازناً دقيقاً بين الكفاءة الحسابية والأداء المتقدم. يعتمد مسار التدريب على ثلاثة مراحل متتابعة تشمل التدريب المتوسط، والضبط الدقيق الخاضع للإشراف، والتعلم التعزيزي المعتمد على خوارزمية CISPO. صُمم النموذج للعمل في بيئتين أساسيتين: بيئة إثبات متعدد الجولات تستقبل ملاحظات المترجم للتحسين الذاتي المستمر، وبيئة وكيل برمجي تتعامل مباشرة مع ملفات النظام لتشغيل الأوامر ومراجعة الأهداف البرمجية في الوقت الفعلي، مما يمكنه من إكمال البراهين المعقدة عبر دورات متعددة من ضغط السياق. سجل Leanstral 1.5 نتائج قياسية على معايير التقييم المعتمدة. فقد استوعب بالكامل مجموعة miniF2F بنسبة 100%، وحل 587 من أصل 672 مشكلة في تحدي Putnam، كما حقق أداءً قياسياً جديداً على معيار FATE-H بنسبة 87% ومعيار FATE-X بنسبة 34%. ويتفوق النموذج على المنافسين بميزانية تكاليف أقل بكثير، حيث تصل تكلفة حل مشكلة إلى نحو 4 دولارات مقابل مئات الدولارات للنماذج المماثلة. كما يظهر النموذج قابلية عالية للتوسع الزمني، حيث يزداد معدل النجاح بشكل مطرد مع زيادة الميزانية الحسابية. يتجاوز التطبيق العملي للنموذج الرياضيات المجردة ليشمل التحقق من صحة الأكواد البرمجية. أثبت النموذج تعقيد وقت شجرة AVL بـ O(log n) عبر أكثر من 2.7 مليون رمز، كما كشف عبر خط أنابيب آلي عن 11 خطأ برمجياً حقيقياً في 57 مستودعاً مفتوح المصدر، منها 5 أخطاء لم تُبلغ عنها المنصات سابقاً. ويوضح هذا قدرة التحقق الرسمي على ملاحقة الثغرات التي تتجاهلها طرق الاختبار التقليدية. تم إطلاق النموذج بشكل كامل على منصة Hugging Face مع توفير واجهة برمجة تطبيقات مجانية للاستخدام المباشر. يوصي المطورون بتكامله عبر بيئة Mistral Vibe وسيرفر Lean LSP MCP لتسهيل عملية البرهان والتصحيح. يعزز هذا الإصدار إتاحة أدوات التحقق الرسمي للمطورين والباحثين بأسعار معقولة، مما يضع حجر أساس لتطبيق منهجيات الصرامة الرياضية على البرمجيات الحديثة.