Theorem.chat بابت
Theorem.chat هڪ حسابي دعويٰ وٺندو آهي ۽ ان کي حل ڪرڻ جي ڪوشش ڪندو آهي. توهان دعويٰ بيان ڪريو ٿا، ۽ معيار جيڪو ان کي ملڻ گهرجي. AI ماڊلز جو هڪ پينل - جيترو توهان چاهيو ٿا، جيڪي به واپارين کان توهان چاهيو ٿا - ان تي حملو ڪري ٿو، ۽ هڪ وڌيڪ ماڊل ريفرينڊس. پوءِ دليل Lean 4 ۾ Mathlib خلاف رسمي طور تي ڪيو ويندو آهي، ۽ ليان ڪارنلز اهو فيصلو ڪندو آهي ته اهو ثبوت آهي يا نه. اهو آخري قدم پيداوار آهي.
ٻيو ماڊل نه پر ڪارنل ڇو؟
ماڊل کي سخت سوال پڇو ۽ توهان کي صحيح يا غلط جو هڪ صاف جواب ملي ويندو. ڪيترن کان پڇو ۽ اهي اڪثر موافق ٿيندا آهن، جيڪو تصديق جي طرح محسوس ٿيندو آهي ۽ نه آهي: ماڊل تربيت جي ڊيٽا شيئر ڪندا آهن ۽ blind spots شيئر ڪندا آهن. ٻيو ماڊل پهريون چيڪ ڪرڻ اڃا تائين هڪ ئي قسم جو فيصلو آهي، ۽ اهو چوڌاري ڳالهايو وڃي ٿو. ليئن ڪارنلز نه ڪري سگهي ٿو. اهو يا ته بيان کي axioms ۽ Mathlib مان نڪتو آهي، يا نه ڪري ٿو، ۽ اعتماد نتيجي تي ڪو اثر نه ٿو پوي.
هڪ رسمي ثبوت کي ٺڳڻ جا عام طريقا چيڪ ڪيا ويا ۽ ان کي رد ڪيو ويو. هڪ ثبوت جيڪو sorry سان هڪ سوراخ ڇڏي ٿو، جيڪو native_decide کي درخواست ڪري ٿو ته ڪنول کي اعتماد تي حساب وٺڻ لاءِ، يا جيڪو هڪ نئون اصول خاموشيءَ سان پيش ڪري ٿو، اهو ڳوليو ويو ۽ ڪاميابي جي حساب سان نه پر ان کي رد ڪيو ويو.
پنل ڇا ڪري سگهي ٿو
بحث ڪرڻ سستو حصو آهي. پينل ادب سان ڪم ڪري ٿو - arXiv، OpenAlex، Crossref - تنهنڪري هڪ ڄاڻايل نتيجو بيان ڪيو ويو آهي نه ته خراب وري- derived. ان ۾ SageMath ۽ PARI/GP ڪمپيوٽر لاءِ، Z3 ۽ CVC5 SMT حل ڪرڻ لاء، OEIS لنڪ جي هڪ سلسلي جي سڃاڻپ لاء ٺهيل آهي، ۽ هڪ sandboxed Python ماحول جنهن ۾ ڪو به نيٽ ورڪ رسائي نه آهي. هڪ اڻڄاتل کي ڏهه هزار ڪيسن جي خلاف آزمائي سگهجي ٿو اڳ ڪنهن به ان کي ثابت ڪرڻ جي ڪوشش ڪرڻ جي ڪوشش ڪري، ۽ هڪ counterexample فوري طور تي بحث کي ختم ڪري ٿو.
ثبوت، نه تقرير
هڪ ميچ argument جي معيار تي نه سکويو ويندو آهي. دعويٰ قبوليت جي معيارن ۾ ورهايل آهي، ۽ معيار صرف ان وقت حل ڪيو ويندو آهي جڏهن ان جي پويان ڪجهه به ٽئين پارٽي طرفان ٻيهر چيڪ ڪري سگهجي ٿو: هڪ ذريعو مناسب پاسي سان نقل ڪيو ويو، يا ڪوڊ جيڪو ان جي حقيقي خروجي سان عمل ۾ آيو. ريفرينڊم ان شواهد کي پاڻ کي فيصلي کان اڳ ٻيهر چيڪ ڪري ٿو، ۽ اهو ميچ کي ختم نه ڪري سگهي ٿو جيستائين معيار اڃان به کوليو هجي.
تو بار مقرر ڪيو
معيار توهان جو چونڊڻ آهي، ۽ ريفرينڊم ان کي لفظن ۾ رکي ٿو. هڪ محتاط ماهر ڇا قبول ڪندو ان لاءِ پڇو ۽ توهان اهو حاصل ڪندا. هر فرض سان گڏ مڪمل استنباطي دليل لاءِ پڇو ۽ توهان ان جي بدران ان جي خلاف فيصلو ڪيو ويندو. هڪ انعام جي پيشڪش جي بار لاءِ پڇو، ۽ سچي نتيجي ۾ عام طور تي هڪ صحيح حساب آهي جتي پينل گهٽ ٿي ويو - جيڪو هڪ اعتماد واري دعوي کان وڌيڪ قيمتي آهي توهان کي پاڻ کي چڪاس ڪرڻ گهرجي.
ان بابت واضح ڪرڻ لاءِ: هيءَ مشين نه آهي جيڪا کوليل مسئلن کي حل ڪري ٿي. هيءَ مشين آهي جيڪا ڪنهن به دليل کي حل ٿيل طور تي پاس ڪرڻ کان انڪار ڪري ٿي جڏهن ته اهو نه آهي، ۽ اهو توهان کي صحيح طرح ٻڌائي ٿو ته ڪهڙو قدم ناڪام ٿيو.
هڪ ناڪام فورمالائزيشن فائديدار نڪتو آھي
جڏهن ليان ثبوت بند نه ڪندو، ته توهان کي صحيح مقصد مليو جيڪو باقي آهي. عملي طور تي اهو تقريبن هميشه اهو جڳهه آهي جتي غير رسمي بحث هٿ ڦيرائڻ هو - اهو قدم هر ڪنهن کي پڙهڻ جي پرزا ورزن اڳيان نڪتو. اهو مقصد پوءِ جنهن جاءِ تي ڏنل آهي جنهن کي حملو ڪرڻ لاءِ بهترين آهي، گڏوگڏ جيڪو اڳ ۾ ئي ڪوشش ڪئي وئي آهي ۽ ٻيو ڪجهه نه. ماڊل thrash جڏهن اهي جڪڙيل آهن، پاڻ کي مڪمل قيمت تي ٻيهر بيان ڪرڻ؛ هڪ مخصوص سوال کي گذرڻ جي بدران عام طور تي ٽوڪنز جي حصي لاءِ بند نه ڪيو ويندو.
ڊگهو ڪم بچي ٿو
هر ليما جيڪو پينل قائم ڪري ٿو سو پنهنجي ثبوت سان گڏ گڏيل ڪتاب ۾ وڃي ٿو، تنهنڪري نتيجا هڪ ڀيرو لکيا ويندا آهن ۽ ڪڏهن به وري نه ٺهرايا ويندا آهن، ۽ بند ٿيل آخرون رڪارڊ ڪيا ويندا آهن ته جيئن ڪوبه ان ۾ واپس نه اچي. ميچ سروس پاسي تي هلندا آهن ۽ صاف وقفو ڪندا آهن - بجيٽ تي، فراهم ڪندڙ جي وقفي تي يا ڇاڪاڻ ته توهان ٽيب بند ڪيو - ۽ جتي وقفو ڪيو ويو آهي اتي ئي وري شروع ڪندا آهن.
هيءَ ڪھڙي لاءِ نه آھي
نظريو هڪ استنباطي لفظ آهي. هي سائيٽ ریاضی، منطق، نظرياتي ڪمپيوٽر سائنس، نظرياتي فزيڪ ۽ اقتصادي نظريو - شعبن لاءِ ٺاهي وئي آهي جتي هڪ دعويٰ ثبوت سان حل ڪئي وئي آهي. بيولوجي، دوا، ڪيميائي يا سماجي سائنس ۾ تجرباتي سوال نظريا پيدا نه ڪندا آهن، اهي نتيجا پيدا ڪندا آهن، ۽ ڪوبه فارملائزيشن جو مقدار انهن کي فيصلو نه ڪندو. اسان جي ڀيڻ سائيٽ referee.chat انھن سوالن لاءِ صحيح طور تي انھن سوالن لاءِ هڪ ئي پينل ۽ ريفريئر عمل کي هلائيندي آهي.