Theorem.chat کے بارے میں
Theorem.chat رياضياتي دعوي ميں ليتا هے اور اس کو حل کر نے کی کوش کرتا هے آپ دعوي کو بيان کريں اور اس کو پورا کر نے کے ليے معيار کو پورا کريں AI ماڈل کا پينل - آپ کو جو چا هيے ، جو بھی وينڈر آپ کو چا هيے - اس پر حملہ کر تا هے اور ایک اور ماڈل ريفرےز اس کے بعد Lean 4 ميں دليل Mathlib کے مقابلے ميں رسمي کر دیا جاتا هے اور لين کرنل ف
ایک کرنل کیوں، اور نہیں ایک دوسرے ماڈل
ماڈل سے سخت سوال پوچھو اور آپ کو صحيح يا غلط کا صاف جواب ملے گا ۔ چند سوال پوچھو اور اکثرا وہ موافق هے ، جو سچائي کا احساس کر تا هے اور نهيں هے ماڈل تربيت کے اعدادو شمار کو شريک کر تا هے اور ندھے نقطے کو شريک کر تا هے ۔ دو سرا ماڈل جس ميں اول ماڈل کي چيک کر نے کيے هيں وہ ابھی تک عين قيادت کا سا ئي قسم هے اور اسکے بارے ميں گفتگو کري جا سکيے لين کرنل نہیں کر سکتا ۔ يا تو اس نے بيان کو Mathlib اور Mathlib سے ليا هے يا اس نے نهيں کريں اور اعتماد کا نتيجے پر کوئی اثر نهيں هے
يه رسمي ثبوت کو فريب کرنے کے معمولي طريقے چيک کيے جا تے هيں اور رد کيے جا تے هيں ۔ يه ثبوت جو sorry ميں اخطار کو چھوڑتا هے ، جو native_decide ميں native_decide کو native_decide کو کرنل کو اعتماد پر حساب ميں لانے کے ليے اپيلا کر تا هے ، يا جو خاموشي سے جديد اصول کو پيش کر تا هے ، تلا ش کيا جاتا هے اور رد کيا جاتا هے نہ کہ اس کو کامیابی کے طور پر شمار کيا جا تا هے
پينل اصل ميں کیا کر سکتا هے
بحث کر نے کا سا ں حصہ هيں پينل ادب کے ساتھ کام کر تا هے arXiv ، OpenAlex ، Crossref ، تو معلوم نتيجہ کو بدتر سے بدتر کر نے کے بجائے SageMath اور PARI/GP کو محاسبے کے ليے استعمال کريں اس ميں SMT حل کر نے کے ليے Z3 اور CVC5 ، OEIS کو ليو کپ کے ليے استعمال کريں اس نے بنا يا هيں اور نیٹ ورک رسائي کے ليے سنڈ باکس پيتھون ماحول کو استعمال کريں کسی کو اس کو ثابت کر نے کے ليے دورہ خرچ کر نے سے پہلے ایک تخمينے کو دس ہزار حالات کے مقابلے ميں آزما يا جا سکتا هے اور يک مثال کے مقابلے ميں فوري طور پر بحث ختم کر دي جا تا هے
ثبوت، نہیں بولنے
match کو استدلال کی معيار پر سکو ري نہیں دهيں جا تا هے.دعا قبولي معيار ميں تقسيم کي جا تا هے اور معيار صرف اس وقت حل کيا جا تا هے جب اس کے پيچھے کا کچھ تھر ے طرف سے دوباره چکا يا جا سکتا هے : متعلقہ نقل کے ساتھ ذريعہ ، يا کوڈ جو اس کے حقيقي آ وٹ پٹ کے ساتھ عمل ميں آتا هے ريفرے فیصلہ کرنے سے پہلے اس ثبوت کو خود دوباره چکا تا هے اور match کو ختم کر نے کا اعلان نہیں کر سکتا جب تک معيار اب تک کھلا هے
آپ بار مقرر
معیار آپ کا انتخاب ہے اور ریفرے اس کو لفظی طور پر رکھتا ہے. ایک محتاط ماہر کے قبول کرنے کے لئے پوچھو اور آپ اسے حاصل کرتے ہیں. ہر فرض کے ساتھ ایک مکمل استنباطی دلیل کے لئے پوچھو اور آپ اس کے برعکس فیصلہ کیے جاتے ہیں. ایک انعام کی پیشکش کے لئے بار کے لئے پوچھو اور سچی نتیجہ عام طور پر ایک صحیح حساب ہے کہ پانل کہاں کم پڑ گیا - جو ایک اعتماد کے دعوے سے زیادہ ہے جو آپ کو خود ہی جانچنا ہوگا.
اس کے بارے میں واضح کرنے کے لئے: یہ ایک مشین نہیں ہے جو کھلے مسائل کو حل کرتا ہے یہ ایک مشین ہے جو ایک دلیل کو حل کی طرح گزرنے سے انکار کرتا ہے جب یہ نہیں ہے، اور یہ آپ کو بتاتا ہے کہ دقیقاً کون سا قدم ناکام ہوا ہے.
فا شل فارمالائزيشن استعمالي خروجي هے
جب لين ثبوت کو بند نہ کر تا هے تو آپ کو عين مقصد ملتا هے جو باقی رہتا هے عملي طور پر تقريبا ہمیشہ اس مقام پر هے جہاں غير رسمي بحث دستي ذبيحہ کر رہا هے ۔ اس قدم پر ہر شخص نے نثري نسخے کو پڑھا هوتا هے اور اس کو گزشتہ وقت تک جھکلا هے ۔ اس مقصد کو پھر اس کے حملے کے ليے جس سيٹ پر بهترين طور پر رکھا جا تا هے اس کے ساتھ جو پہلے سے آزما هو چکا هے اور اور کچھ نهيں ۔ ماڈل ں کو جب رکاوٹ آ جا تا هے تو تير ميں لگ جاتا هے ، پورے خرچ پر خود کو دو باره بيان کر تا هے ۔ اسکے بدلے ایک خاص سوال کو گزيرا کر نے سے اکثر تو کينز کے ایک حصے کے ليے بندش کو کھول دیا جا تا هے
طویل کام زندہ رہتا ہے
ہر لیمما پینل قائم اس کے ثبوت کے ساتھ ایک مشترکہ لیڈر میں جاتا ہے، تو نتائج ایک بار لکھا جاتا ہے اور کبھی دوبارہ حاصل نہیں ہوتا، اور بیکار انتہا ریکارڈ کیا جاتا ہے تو کوئی بھی ان میں واپس چلتا ہے. Matches سرور جانب چلتے ہیں اور صاف ٹھیرتے ہیں - بجٹ پر، ایک فراہم کرنے والے کے قطع یا کیونکہ آپ نے ٹیب بند کیا - اور وہ ٹھیک وہاں سے شروع کرتے ہیں جہاں وہ ٹھر گئے.
یہ کیا ہے کے لئے نہیں ہے
تئورم يه تنازل کا لفظ هے ۔ یہ سا يط رياضيات ، منطق ، نظري کمپیوٹر سائنس ، نظري طبعيات اور معاشي نظريه کے ليے بنا يا گيا هے ۔ جن ميں ايک دعوي کو ثبوت کے ليے حل کر يا جا تا هے ۔ بيولوجي ، طب ، کيميائي يا سماجي سائنس کے تجرباتي سوالات تئورم بناتے هيں نہيں ، وہ نتيجے بناتے هيں اور ان کا فیصلہ سرا عات کا کوئی مقدار نہیں کر سکتا ۔ ہمارے referee.chat سا يط ميں عين عين سوالات کے ليے لين قدم کے ليے عين عين پينل اور ريفرے عمل چلتا هے