دعویٰ بیان کریں. کرنل فیصلہ کرتا ہے کہ یہ ثابت کیا گیا ہے.

ماڈل کا پينل آپکے مسئلے پر ادب ، SageMath ، PARI/GP اور اس ايم ٹی حل کر نے والے کے ساتھ حملہ کرتا هے ، پھر Mathlib کے مقابلے ميں Lean 4 ميں نتيجے کو رسمي بنا تا هے ليان کا کرنل يا تو ثبوت کو قبول کر تا هے يا تو نہیں اور اس کو تبديل کر نے کے ليے کوئی اعتماد کا اندازہ نهيں هے جب اس ميں ناکامي آ تا هے تو آپکو عين مقصد ملتا هے جو باقی رہتا هے ، جو عام طور پر غير رسمي بحث کے ليے دستي ہلکا ں هوتا هے

مقصد
خاص طور پر سوچيں کيا کريں يعني کیا کريں 'فرض کريں کيا X سچ ه هے اور اس کو ثابت کريں 'مجھے X کے متعلق بتايں
بار یہ صاف کرنے کے لئے ہے
ريفرے اس بار کو لفظي طور پر رکھتا هے. اجر سطحي ثبوت کے ليے پوچھيں اور جب پينل کمي ميں آتا هے تو آپ کو صاف بتا تا هے ، فزنس اعلان کر نے کے بدلے
پينل
زیادہ سیٹوں کا مطلب زیادہ زاویوں، اور ہر راؤنڈ میں زیادہ خرچ.
ريفرے
معیار پر قوانین اور دوبارہ-چک شواہد کے ہر ٹکڑے کی اپنی سب سے مضبوط ماڈل کے قابل.
دور
خرچ کی حد
اسے مارنے سے match کو روک دیا جاتا ہے کچھ بھی نہیں کھویا جاتا ہے.
د
match شروع کرنے کے لئے رجسٹر
نئے اکاؤنٹس کو شروع کریڈٹ ملتا ہے، ایک حقیقی match کے لئے کافی.
ایک چيکر جو متقاعد نہیں کريے جا سکتے هيں

Mathlib کے ساتھ Lean 4 آخري بياني کو تا ئن چک کر تا هے اور sorry ، native_decide يا جديد اصول پر مبنی ثبوت کو شمار کر نے کے بجائے رد کر دیا جاتا هے اس کے ساتھ SageMath ، PARI/GP ، Z3 ، CVC5 اور OEIS ، اس ليے کوئي اسکے متعلق کچھ ثابت کر نے کے ليے کوئي کوشش کرے اس سے پہلے کوئي بنا ئش کو حساب اور شناخت کر سکيے جا سکتا هے

ایک ناکام ثبوت ایک تلاش ہے

جب رسمیت ناکام ہو جاتی ہے، تو وہ مقصد جو لین بند نہیں کر سکتا اس کو اس پر حملہ کرنے کے لئے بہترین جگہ پر پہنچایا جاتا ہے: صرف وہ مقصد، نہ کہ پوری تاریخ۔ ایک رد شدہ ثبوت فاصلے کا نام صحیح طور پر دیتا ہے، جو اکثر غیر رسمی بحثوں سے زیادہ ہے۔

کچھ بھی دو بار ثابت ہے

هر ليما جو پينل قائم کر تا هے اسکے ثبوت کے ساتھ شريک ليڈر ميں جا تا هے ، تو هيں هي