دعويٰ بيان ڪريو. ڪارنل فيصلو ڪندو ته ڇا اهو ثبوت آهي.

ماڊلن جو هڪ پينل ادب، SageMath، PARI/GP ۽ SMT حل ڪندڙ سان توهان جي مسئلي تي حملو ڪري ٿو، پوءِ نتيجي کي Lean 4 ۾ Mathlib جي مقابلي ۾ رسمي ڪري ٿو. ليان جو ڪنول يا ته ثبوت قبول ڪري ٿو يا نه ڪري ٿو، ۽ ڪوبه اعتماد واري پرسي جو مقدار ان کي تبديل نه ڪندو آهي. جڏھن اھو ناڪام ٿئي ٿو ته توھان کي صحيح مقصد ملي ٿو جيڪو رھندو آھي، جتي عام طور تي غير رسمي بحث ھٿ ڦيرائڻ ھو.

مقصد
خاص طور تي ڄاڻايو ته ڇا ڪيو ويو آهي. 'فڪس ڪريو ته X سچو آهي، ۽ اهو ثابت ڪريو ته' بيٽس 'مونکي X بابت ٻڌايو.
بار صاف ڪرڻو پوندو
ريفرينڊم ان بار کي لفظي طور تي رکي ٿو. انعام جي سطح جي ثبوت لاءِ پڇو ۽ اهو توهان کي واضح طور تي چوندو جڏهن پينل مختصر ٿي ويندو ، ڪاميابي جي اعلان ڪرڻ جي بدران.
پني
وڌيڪ جڳهن جو مطلب وڌيڪ زاويه ۽ هر دور جي وڌيڪ قيمت آهي.
ريفريئر
معيار تي رائلز ۽ هر شيءَ جو ٻيهر چڪاس ڪري ٿو.
رانديون
خرچ جي حد
ان کي دٻائڻ سان راند وقف ٿيندي. ڪابه شيءِ وڃائي نه ويندي.
ڏسڻ وارو
ميچ شروع ڪرڻ لاءِ رجسٽر ٿيو
نئون اڪائونٽ شروع ڪريڊٽ حاصل ڪري ٿو، هڪ حقيقي ميچ لاءِ ڪافي.
هڪ چيڪ جيڪو يقيني بڻائي نه ٿو سگهجي

Lean 4 سان Mathlib قسم-چڪون آخري بيان، ۽ هڪ ثبوت ته sorry تي ڦري native_decide يا تازو axiom جي ڀيٽ ۾ ڳڻپ نه رد ڪيو ويو آهي. ان سان گڏ: SageMath، PARI/GP، Z3، CVC5 ۽ OEIS، ته جيئن هڪ تعمير جي اڳ ۾ ڪنهن به ان بابت ڪجهه ثابت ڪرڻ جي ڪوشش ڪئي آهي ڳڻپ ۽ سڃاڻپ ڪري سگهجي ٿو.

هڪ ناڪام ثبوت هڪ ڳولا آهي

جڏهن رسميت ناڪام ٿئي ٿي، ته اهو مقصد جيڪو لينن نه ٿو بند ڪري سگهي، ان کي ڪنهن به جاءِ تي منتقل ڪيو ويندو آهي جيڪو ان تي حملو ڪرڻ لاءِ بهترين آهي: صرف اهو مقصد، نه ته سڄي تاريخ. هڪ رد ٿيل ثبوت فاصلي جو نالو صحيح طور تي رکي ٿو، جيڪو اڪثر غير رسمي بحثن کان وڌيڪ آهي.

ڪابه شيءِ ٻه ڀيرا ثابت نه ٿي ٿئي

هر ليما جيڪو پينل قائم ڪري ٿو سو ان جي ثبوت سان گڏ گڏيل ڪتاب ۾ وڃي ٿو، تنھنڪري ان کي وري ڪڏھن نه ٺاھيو ويندو آھي ۽ اڻ ٺاھيون پڇاڙيون وري ڪڏھن نه ڪوشش ڪيون وينديون آھن. ڊگھا مسئلا ڪم وڃائڻ کانسواءِ وقف ۽ جاري ڪيا ويندا آھن: ٽيب بند ڪريو ۽ سڀاڻي موٽي اچو.