دعويٰ بيان ڪريو. ڪارنل فيصلو ڪندو ته ڇا اهو ثبوت آهي.
ماڊلن جو هڪ پينل ادب، SageMath، PARI/GP ۽ SMT حل ڪندڙ سان توهان جي مسئلي تي حملو ڪري ٿو، پوءِ نتيجي کي Lean 4 ۾ Mathlib جي مقابلي ۾ رسمي ڪري ٿو. ليان جو ڪنول يا ته ثبوت قبول ڪري ٿو يا نه ڪري ٿو، ۽ ڪوبه اعتماد واري پرسي جو مقدار ان کي تبديل نه ڪندو آهي. جڏھن اھو ناڪام ٿئي ٿو ته توھان کي صحيح مقصد ملي ٿو جيڪو رھندو آھي، جتي عام طور تي غير رسمي بحث ھٿ ڦيرائڻ ھو.
هڪ چيڪ جيڪو يقيني بڻائي نه ٿو سگهجي
Lean 4 سان Mathlib قسم-چڪون آخري بيان، ۽ هڪ ثبوت ته sorry تي ڦري native_decide يا تازو axiom جي ڀيٽ ۾ ڳڻپ نه رد ڪيو ويو آهي. ان سان گڏ: SageMath، PARI/GP، Z3، CVC5 ۽ OEIS، ته جيئن هڪ تعمير جي اڳ ۾ ڪنهن به ان بابت ڪجهه ثابت ڪرڻ جي ڪوشش ڪئي آهي ڳڻپ ۽ سڃاڻپ ڪري سگهجي ٿو.
هڪ ناڪام ثبوت هڪ ڳولا آهي
جڏهن رسميت ناڪام ٿئي ٿي، ته اهو مقصد جيڪو لينن نه ٿو بند ڪري سگهي، ان کي ڪنهن به جاءِ تي منتقل ڪيو ويندو آهي جيڪو ان تي حملو ڪرڻ لاءِ بهترين آهي: صرف اهو مقصد، نه ته سڄي تاريخ. هڪ رد ٿيل ثبوت فاصلي جو نالو صحيح طور تي رکي ٿو، جيڪو اڪثر غير رسمي بحثن کان وڌيڪ آهي.
ڪابه شيءِ ٻه ڀيرا ثابت نه ٿي ٿئي
هر ليما جيڪو پينل قائم ڪري ٿو سو ان جي ثبوت سان گڏ گڏيل ڪتاب ۾ وڃي ٿو، تنھنڪري ان کي وري ڪڏھن نه ٺاھيو ويندو آھي ۽ اڻ ٺاھيون پڇاڙيون وري ڪڏھن نه ڪوشش ڪيون وينديون آھن. ڊگھا مسئلا ڪم وڃائڻ کانسواءِ وقف ۽ جاري ڪيا ويندا آھن: ٽيب بند ڪريو ۽ سڀاڻي موٽي اچو.