ذكر الادعاء، وتقرر النواة ما إذا كان قد تم إثباته.

Lean 4 مع Mathlib تحقق من نوع البيان النهائي، والدليل الذي يعتمد على sorry، native_decide أو بديهية جديدة يرفض بدلا من أن يحسب. إلى جانبه: SageMath، PARI/GP، Z3، CVC5 وOEIS، بحيث يمكن حساب البناء وتحديده قبل أن يحاول أي شخص إثبات أي شيء عنه.

عندما يفشل إضفاء الطابع الرسمي، فإن الهدف الذي لم يتمكن لين من إغلاقه يسلم إلى أي مقعد يكون في أفضل وضع لمهاجمة ذلك الهدف: ذلك الهدف فقط، وليس التاريخ بالكامل. ويحدد الدليل المرفوض الفجوة بدقة، وهو ما يفوق ما تفعله أغلب الحجج غير الرسمية على الإطلاق.

إن كل مشكلة تحددها الهيئة توضع في دفتر أستاذ مشترك مع البرهان، لذا فلا يعاد استقاؤها أبدا ولا يعاد محاولة الحلول في المآزق أبدا. ويتم تعليق المشاكل الطويلة واستئنافها دون فقدان العمل: أغلق العلامة والعودة إلى الغد.