داواکاریەکەت بنووسە. خانەی وێب بڕیار دەدات کە ئایا ڕاستیەکەت پەسەند کراوە یان نا.

پەڕەی نمونە هێرش دەکاتە سەر کێشەکەت بە ئەدەبیات، SageMath، PARI/GP و چارەسەرکەری SMT، پاشان ئەنجامەکە بە شێوەی فەرمی دەکات لە Lean 4 بەرامبەر Mathlib. خانەی لیەن یان بەڵگە قبوڵ دەکات یان قبوڵی ناکات، وە هیچ بڕێکی دڵنیای ناگۆڕێت. کاتێک شکست دەهێنیت ئامانجی ڕاستەقینە بەدەست دەهێنیت کە ماوەتەوە، کە بە گشتی ئەو شوێنەیە کە وتووێژێکی نافەرمی دەستی لێدابوو.

ئامانج
بە تایبەت بە مەبەستی چی ئەنجام دراوە. 'بەڕێوەبەری ئەگەر X ڕاست بێت، وە نیشانی بدە' دێت 'بەبارەی X پێم بڵێ'
باڕەکە پێویستە پاک بکرێتەوە
دادوەر بە ڕاستەوخۆ ئەم بارە دەگرێت. داوا لە بەڵگەیەکی پلەی خەڵات بکە و بە ئاشکرا پێت دەڵێت کاتێک پانێلەکە کورت دەبێتەوە، نەک ڕاگەیاندنی سەرکەوتن.
پانێلەکە
شوێنی زیاتر مانای زاراوەی زیاترە و نرخی زیاترە بۆ هەر دورەیەک.
دادوەر
یاساکان لەسەر بنەمای ڕێساکان و پشکنینی هەموو به‌ڵگەکان، بە نرخی بەهێزترین نمونە
خولەک
سنووری خەرجکردن
بە لێدانى یاریەکە ڕادەگرێت. هیچ شتێک لەدەست نادرێت.
بینینی
بۆ دەستپێکردنی یاریەکە تۆماربکە
حسابە نوێیەکان پارەی دەست پێکردنیان پێدەدرێت، کە بۆ یاری ڕاستەقینە پێویستن.
پشکنەرێک کە ناکرێت ڕازی بکرێت

Lean 4 لەگەڵ Mathlib جۆری پشکنینی دوایین وتەیە، وە بەڵگەیەک کە لەسەر sorry، native_decide یان ئەکسیۆمێکی تازەیە پشتگوێ دەخرێت لەجیاتی ئەوەی بژمێردرێت. لە نزیکەوە: SageMath، PARI/GP، Z3، CVC5 و OEIS، بۆیە دروستکردنی دەتوانرێت حساب بکرێت و ناسێنرێت پێش ئەوەی کەس هەوڵ بدات هیچ شتێک لەسەر ئەوە بسەلمێنێت.

بەڵگەیەکی شکستخواردوو دۆزینەوەیەکە

کاتێک رێکخستن شکست دەهێنێت، ئامانجی لیۆن نەتوانیوە ببەستێتەوە بە هەر شوێنێک کە باشترین شوێنە بۆ هێرشکردنە سەر: تەنها ئەو ئامانجە، نەک هەموو مێژوویەکە. بەڵگەیەکی ڕەتکراو ناوی ئەو شکانەیە بە شێوەیەکی ڕاستەوخۆ، کە زیاترە لە زۆربەی وتووێژەکانی نافەرمی.

هیچ شتێک دووجار تاقی ناکرێتەوە

هەر لۆمێ کە پانێلەکە دادەنێت لە پەڕەیەکی هاوبەشدا دەچێت لەگەڵ بەڵگەکەی، بۆیە هەرگیز دووبارە دروست ناکرێتەوە و کۆتاییەکانیش هەرگیز هەوڵ نادرێت. کێشە درێژەکان ڕادەوەستێن و بەردەوام دەبن بەبێ لەدەستدانی کار: پەڕەکە ببەستەوە و سبەینێ بگەڕەوە.