لين (مساعد إثبات)

Lean هو مساعدٌ لإثبات البراهين ولغة برمجة وظيفية . ^{[ 2 ]} وهو مبنيٌّ على حساب الإنشاءات مع الأنواع الاستقرائية (وتحديدًا، حساب الإنشاءات الاستقرائية)، وهي نظرية الأنواع الأساسية التي طُوِّرت في الأصل مع مُثبت النظريات Coq ، ^{[ 3 ]} والذي أُعيد تسميته إلى Rocq في عام 2024. ^{[ 4 ]} وهو مشروع برمجي مجاني ومفتوح المصدر مُستضاف على GitHub . ويتلقى التطوير حاليًا دعمًا من منظمة Lean Focused Research Organization (FRO) غير الربحية .

تم تطوير Lean بشكل أساسي من قبل عالم الكمبيوتر البرازيلي ليوناردو دي مورا أثناء عمله في مايكروسوفت للأبحاث والآن أمازون لخدمات الويب ، وقد حظي بمساهمات كبيرة من مؤلفين مشاركين ومتعاونين آخرين خلال تاريخه.

تم إطلاقها في عام 2013، ^{[ 5 ]} كانت الإصدارات الأولية من اللغة، والمعروفة لاحقًا باسم Lean 1 و2، تجريبية وتحتوي على ميزات مثل دعم الأسس القائمة على نظرية نوع التماثل والتي تم إسقاطها لاحقًا.

كان Lean 3 (الذي صدر لأول مرة في 20 يناير 2017) أول إصدار مستقر إلى حد ما من Lean. تم تنفيذه بشكل أساسي بلغة C++ مع بعض الميزات المكتوبة بلغة Lean نفسها. بعد الإصدار 3.4.2، انتهى دعم Lean 3 رسميًا بينما بدأ تطوير Lean 4. خلال هذه الفترة الانتقالية، قام أعضاء مجتمع Lean بتطوير وإصدار نسخ غير رسمية حتى الإصدار 3.51.1. ^{[ 6 ]}

في عام 2021، تم إصدار Lean 4، وهو عبارة عن إعادة تنفيذ لبرنامج Lean لإثبات النظريات، قادر على إنتاج كود C يتم تجميعه لاحقًا، مما يتيح تطوير أتمتة فعالة خاصة بمجال معين. ^{[ 7 ]} كما يحتوي Lean 4 على نظام ماكرو مُحسَّن ، بالإضافة إلى تحسينات في توليف فئات الأنواع وإجراءات إدارة الذاكرة مقارنةً بالإصدار السابق. ^{[ 8 ]} ومن المزايا الأخرى مقارنةً بـ Lean 3، إمكانية تجنب تعديل كود C++ لتعديل الواجهة الأمامية والأجزاء الرئيسية الأخرى من النظام الأساسي، حيث تم تنفيذها جميعًا الآن باستخدام Lean، وهي متاحة للمستخدم النهائي لتعديلها حسب الحاجة. ^{[ 2 ]}

لا يتوافق Lean 4 مع الإصدارات السابقة من Lean 3. ^{[ 9 ]} وهو يستخدم إصدار C++17 من لغة C++. ^{[ 2 ]}

في عام 2023، تم تشكيل Lean FRO، بهدف تحسين قابلية التوسع وسهولة الاستخدام للغة، وتنفيذ أتمتة البرهان . ^{[ 10 ]}

في عام 2025، مُنحت جائزة ACM SIGPLAN لبرمجيات لغات البرمجة إلى غابرييل إبنر، وسونهو كونغ، وليو دي مورا، وسيباستيان أولريش عن منهج Lean، وذلك لتأثيره الكبير على الرياضيات، والتحقق من الأجهزة والبرمجيات، والذكاء الاصطناعي. ^{[ 11 ]}

في عام 2026، حصلت مكتبة mathlib على جائزة Demailly للعلوم المفتوحة . ^{[ 12 ]}

تتضمن لغة Lean العديد من الميزات المفيدة للبرمجة الوظيفية وإثبات النظريات، مثل الأنواع التابعة ، وفئات الأنواع ، والتعددية الخيطية، ولغة تكتيكية معبرة، ونظام الوحدات النمطية. ^{[ 13 ]}

يمكن تعريف الأعداد الطبيعية بأنها نوع استقرائي . يستند هذا التعريف إلى بديهيات بيانو ، وينص على أن كل عدد طبيعي إما أن يكون صفرًا أو العدد التالي لعدد طبيعي آخر.

طبيعي استقرائي : النوع | صفر : طبيعي | متتالي : طبيعي → طبيعي

يمكن تعريف عملية جمع الأعداد الطبيعية بشكل تكراري ، باستخدام مطابقة الأنماط .

دالة Nat.add : Nat → Nat → Nat | n , Nat.zero => n -- n + 0 = n | n , Nat.succ m = > Nat.succ ( Nat.add n m ) -- n + succ(m) = succ ( n + m )

هذا برهان بسيط على${\displaystyle (P\wedge Q)\implies (Q\wedge P)}$بالنسبة لقضيتين P و Q ( حيث${\displaystyle \wedge }$هو حرف العطف و${\displaystyle \implies }$( الاستنتاج ) في منهجية Lean باستخدام الوضع التكتيكي:

نظرية and_swap ( p q : Prop ) : p ∧ q → q ∧ p := حسب المقدمة h -- بافتراض p ∧ q مع البرهان h، يكون الهدف هو q ∧ p تطبيق And . المقدمة -- ينقسم الهدف إلى هدفين فرعيين، أحدهما هو q والآخر هو p · exact h . right -- الهدف الفرعي الأول هو الجزء الأيمن من h بالضبط : p ∧ q · exact h . left -- الهدف الفرعي الثاني هو الجزء الأيسر من h بالضبط : p ∧ q

وهذا البرهان نفسه في وضع المصطلح:

نظرية and_swap ( p q : Prop ) : p ∧ q → q ∧ p := fun ⟨ hp , hq ⟩ => ⟨ hq , hp ⟩

يمكن أيضًا إثبات النظرية باستخدام أسلوب الطحن، الذي يستخدم تقنيات من برامج حل SMT لإنشاء البراهين تلقائيًا:

نظرية and_swap ( p q : Prop ) : p ∧ q → q ∧ p := by grind

• النوع التابع
• قائمة مساعدي التدقيق
• mimalloc
• نظرية الأنواع

• الموقع الرسمي
• اعتمد على GitHub
• مجتمع لين
• Lean FRO
• لعبة الأعداد الطبيعية - برنامج تعليمي تفاعلي لتعلم منهجية لين
• Moogle.ai - محرك بحث دلالي للعثور على النظريات في مكتبة الرياضيات