په اړه Theorem.chat
Theorem.chat د ریاضی ادعا کوي او هڅه کوي چې دا حل کړي. تاسو ادعا کوئ، او معیاري دا باید سره وګوري. د AI ماډلونو یوه ډله - لکه څنګه چې تاسو غواړئ، له کوم څخه چې تاسو غواړئ - دا برید کوي، او یو نور ماډل راجع کوي. بیا د دلیل په Mathlib خلاف Lean 4 کې رسمي کیږي، او د Lean kernel پریکړه کوي که دا ثابته شي. هغه وروستی ګام محصول دی.
ولې يو هسته، او نه بل ماډل
د ماډل څخه سخته پوښتنه وپوښتئ او تاسو د یو روان ځواب ترلاسه کوئ که دا سم وي یا نه. څو پوښتنې وکړئ او دوی اکثرا موافق دي، کوم چې د تایید په څیر احساس کوي او نه دی: ماډلونه د روزنې معلومات شریکوي او د ړندو ځایونو شریکوي. یو بل ماډل چې لومړی یې چک کوي لاهم د قضاوت ورته ډول دی، او دا کولی شي د دورې خبرې وکړي. د لیون کرنل نشي کولی. دا یا د axioms او Mathlib څخه بیان راځي، یا دا نه کوي، او باور د پایلو په اړه هیڅ اغیزه نلري.
د عادي لارو د يو رسمي ثبوت د جعل لپاره چک او رد شوي دي. يو ثبوت چې سره sorry يوه سوري پرېږدي، يو چې native_decide ته د غوښتنې د kernel په باور د يو محاسبه، يا يو چې په خاموشۍ سره د يو نوي axiom معرفي کوي، کشف او رد نه د بریالیتوب په توګه د شمېرل.
څۀ چې چوکاټ په رښتيا کې کولای شي
د استدلال کولو ارزانه برخه ده. د پینل د ادبیاتو سره کار کوي - arXiv، OpenAlex، Crossref - نو یو پیژندل شوی پایله د بد بدیل په پرتله یادونه کیږي. دا د محاسبې لپاره SageMath او PARI/GP لري، Z3 او CVC5 د SMT حل کولو لپاره، د OEIS لټون د ترتیب پیژندلو لپاره چې دا یې جوړ کړی، او د شبکې لاسرسی پرته د سانډبکس پیټین چاپیریال. یو اټکل کیدی شي د دېرش زره قضیو پروړاندې ازمول شي مخکې له دې چې څوک د دې ثابتولو هڅه وکړي، او یو counterexample د بحث په فوري توګه پای ته رسیږي.
شواهد، نه د تعبير
د يوې لوبې په استدلال د کیفیت نه ده د امتیاز. د ادعا په قبول معيارونو کې تقسيميږي، او يو معيار يوازې کله چې د هغه شاته څه شي کولای شي د يوې دريم ګوند له خوا بيا کتنه: د اړونده نقل نقل سره د يو سرچينه نقل، يا کوډ چې په حقيقت کې د خپل حقيقي محصول سره اجرا شو. د قاضيانو بيا کتنه چې شواهد د حكم کولو څخه مخکې ځان، او دا نشي کولای د لوبې پای اعلان کړي، په داسې حال کې چې يو معيار لا هم پرانستل.
تاسو د بار ټاکلې
د معیار معیار ستاسو انتخاب دی، او د ناظر دا په لفظي ډول لري. د هغه څه لپاره وپوښتئ چې یو محتاط متخصص به ومني او تاسو به دا ترلاسه کړئ. د هر انګیرنې سره د بشپړ استنباطي دلیل لپاره وپوښتئ او تاسو به د دې پرځای د دې پروړاندې قضاوت وکړئ. د بار لپاره وپوښتئ چې د جایزه وړاندې کول به مخ ته راشي، او د صادقانه پایله معمولا د دقیق حساب دی چې چیرته د پینل لنډ و - کوم چې د یو باور لرونکي ادعا څخه ډیر ارزښت لري چې تاسو به په هرصورت ځان وګورئ.
د دې په اړه ساده وي: دا نه ده چې د يو ماشين چې پرانستې ستونزې حل. دا يو ماشين چې نه غواړي چې د يو دليل د تېرېدو په توګه حل کله چې دا نه دی، او چې تاسو ته وايي په سمه توګه چې کوم ګام ناکامه.
يو ناکام formalization د ګټور خروجي ده
کله چې Lean به ثبوت بند نه کړي، تاسو به د دقیق هدف ترلاسه کړئ چې پاتې کیږي. په عمل کې دا نږدې تل هغه ځای دی چیرې چې غیر رسمي دلیل د لاس په ویلو و - د هر چا د پروزې نسخه لوستل به د تیرو وختونو په څیر وي. دا هدف بیا هغه څوک ته ورکړل کیږي چې د هغه برید کولو لپاره غوره ځای لري، د هغه څه سره چې دمخه هڅه شوې، او نور هیڅ نه. ماډلونه کله چې دوی ونیول شي، په بشپړه توګه په بشپړه توګه ځان ته بیا وده ورکوي؛ د یو ځانګړي پوښتنې په ځای د توکو د یوه برخې لپاره د توکو د یوې برخې لپاره د یوې ځانګړې پوښتنې په ځای د یوې ځانګړې پوښتنې په ځای د یوې ځانګړې پوښتنې په ځای د یوې ځانګړې پوښتنې په ځای د یوې ځانګړې پوښتنې په ځای د یوې ځانګړې پوښتنې په ځای د یوې ځانګړې پوښتنې په ځای.
اوږد کار ژوندی پاتې کيږي
هر لیما چې د پینل تاسیس کوي د خپل ثبوت سره یو شریک لیګ ته ځي، نو پایلې یو ځل لیکل کیږي او هیڅکله بیا نه راځي، او مړینې ثبت شوي نو هیڅوک یې بیرته نه ځي. د سرورونو سرور خوا ته ځي او پاک وقفه - په بودیجه، د چمتو کونکي په وقفه کې، یا ځکه چې تاسو ت buttonۍ وتړله - او دقیقا چیرته چې دوی ودرېدل.
دا د څه لپاره نه دی
تیورم یو استنباطي کلمه ده. دا سایټ د ریاضیاتو، منطق، نظری کمپیوټر ساینس، نظری فزیک او اقتصادي تیوري لپاره جوړ شوی - هغه ساحې چې ادعا د ثبوت لخوا حل کیږي. په بیولوژي، درمل، کیمیا یا ټولنیزو علومو کې تجربوي پوښتنې تیورم نه تولیدوي، دوی موندنې تولیدوي، او د رسمي کولو هیڅ مقدار به یې پریکړه وکړي. زموږ خویندې سایټ referee.chat د لیون ګام پرته د ورته پینل او ریفری پروسې چلوي، دقیقا د هغو پوښتنو لپاره.