အကြောင်းကို Theorem.chat
Theorem.chat သင်္ချာဆိုင်ရာတောင်းဆိုချက်တစ်ခုယူပြီး၎င်းကိုဖြေရှင်းဖို့ကြိုးစား. သင်ကတောင်းဆိုချက်ကိုဖော်ပြ, နှင့်စံချိန်စံညွှန်းကိုတွေ့ဆုံရန်ရှိသည်. AI ကိုမော်ဒယ်များ၏ panel ကို - သင်လိုချင်သောအတိုင်းများစွာသော, သင်လိုချင်သောမည်သည့်ရောင်းချသူမှ - ဒါကိုတိုက်ခိုက်, နှင့်တစ်ဦးပိုမိုမော်ဒယ် referees. ထိုအခါအငြင်းပွားမှု Lean 4 Mathlib အပေါ် formalized ခံရ, နှင့် Lean kernel ကသက်သေပြခဲ့သည်မဟုတ်ကြောင်းဆုံးဖြတ်. ထိုနောက်ဆုံးအဆင့်မှာထုတ်ကုန်ဖြစ်ပါသည်.
ဘာကြောင့် kernel ကိုနှင့်အခြားမော်ဒယ်မဟုတ်ပါ
တစ်ခု model ကိုတစ်ဦးခက်ခဲမေးခွန်းကိုမေးပါနှင့်သင်သည်အမှန်ဖြစ်ပါစေသို့မဟုတ်မဟုတ်ပါကြောင်း fluent အဖြေတစ်ခုရ. များစွာသောမေးမြန်းနှင့်သူတို့မကြာခဏသဘောတူ, တစ်ခု corroboration ကဲ့သို့ခံစားရပြီးမဟုတ်ပါဘူး: models များလေ့ကျင့်ရေးဒေတာမျှဝေနှင့်အမြင်အာရုံအညစ်အကြေးမျှဝေ. ပထမဦးဆုံးစစ်ဆေးခြင်းတစ်ဦးဒုတိယမော်ဒယ်ကယခုတိုင်ပင်ဆွေးနွေးနိုင်ပါတယ်, နှင့်အပတ်စဉ်ပြောဆိုနိုင်ပါတယ်. အဆိုပါ Lean kernel ကိုမနိုင်. ဒါဟာ axioms နှင့် Mathlib မှထုတ်ပြန်ချက်ကို derivates, ဒါမှမဟုတ်မဟုတ်ပါဘူး, နှင့်ယုံကြည်မှုရလဒ်အပေါ်အကျိုးသက်ရောက်မှုမရှိ.
sorry နှင့်အတူအပေါက်တစ်ခုထွက်ခွာသောသက်သေအထောက်အထား, native_decide အပေါ်အတည်ပြုချက်အပေါ်ကွန်ပျူတာတစ်ဦးက compute လုပ်ဖို့တစ်ဦးကို appeals တစ်ခု, သို့မဟုတ်တိတ်ဆိတ်စွာအသစ်တစ်ခု axiom ကိုမိတ်ဆက်တစ်ခု, အောင်မြင်မှုအဖြစ်စာရင်းမသွင်းဘဲထက် detected နှင့်ငြင်းပယ်ခံရသည်။
ပင်မမျက်နှာပြင်က တကယ်လုပ်နိုင်တာ
ငြင်းခုံမှုသည်စျေးပေါအပိုင်းဖြစ်ပါသည်. အဆိုပါ panel ကိုစာပေနှင့်အတူအလုပ်လုပ် - arXiv, OpenAlex, Crossref - ဒါကြောင့်သိသိသာသာရလဒ်ဆိုးရွားစွာ re-derived ထက်ပိုပြီးအကြံပြုထားသည်. ဒါဟာ SageMath နှင့် PARI/GP ကွန်ပျူတာများအတွက်ရှိပါတယ်, Z3 နှင့် CVC5 SMT ဖြေရှင်းရန်, OEIS တည်ဆောက်ခဲ့သည် sequence ကိုခွဲခြားသတ်မှတ်ဖို့ရှာဖွေရေး, နှင့် sandboxed Python ပတ်ဝန်းကျင်ကိုမဆိုကွန်ရက် access ကိုနှင့်အတူ. မည်သူမဆိုကသက်သေပြဖို့ကြိုးစားနေတစ်ပတ်လည်ကုန်ကျစရိတ်မတိုင်မီတစ်ဦးခန့်မှန်းချက်ကိုထောင်ပေါင်းများစွာ၏ကိစ္စရပ်များအပေါ်စမ်းသပ်နိုင်ပါတယ်, နှင့် counterexample ချက်ချင်းဆွေးနွေးမှုအဆုံးသတ်.
သက်သေအထောက်အထား, မ eloquence
တစ်ဦးကို match အကြောင်းပြချက်အရည်အသွေးအပေါ် scored မဟုတ်. အဆိုပါတောင်းဆိုချက်လက်ခံမှုစံနှုန်းများထဲသို့ခွဲထုတ်သည်, နှင့်စံနှုန်းတစ်ခုနောက်ကွယ်မှတစ်ခုခုတတိယပါတီမှ re-စစ်ဆေးနိုင်သည်သောအခါသာ settled ဖြစ်ပါတယ်။ အဆိုပါအဆက်အသွယ် passage ကို quoted အတူအရင်းအမြစ်, သို့မဟုတ်တကယ်တော့၎င်း၏အစစ်အမှန် output ကိုနှင့်အတူ executed ခဲ့သည်ကကုဒ်. အဆိုပါ arbitrator ဆုံးဖြတ်ချက်မတိုင်မီသက်သေအထောက်အထားကိုယ်ပိုင် re-စစ်ဆေး, နှင့်စံနှုန်းတစ်ခုအစဉ်အဆက်ဖွင့်နေစဉ်ပွဲစဉ်ပြီးဆုံးကြေညာနိုင်.
သင်ကဘား set
စံချိန်စံညွှန်းရွေးချယ်ဖို့သင့်ရဲ့ဖြစ်ပါသည်, နှင့်အငြင်းပွားမှုအဆုံးသတ်သူသည်အမှန်တကယ်က၎င်းကိုကိုင်ထား. သတိထားအထူးကုလက်ခံမည်နှင့်သင်ကရလိမ့်မယ်ဘာကိုမေး. အားလုံးယူဆချက်ကိုဖော်ပြထားနှင့်အတူအပြည့်အဝ deductive ငြင်းခုံအတွက်မေးမြန်းနှင့်သင်ကအစားထိုသို့အကြမ်းဖက်မှုအပေါ်တရားစီရင်ခံရဖို့ရ. ဆုပေးပွဲတင်သွင်းမှုရင်ဆိုင်ရမည်ဖြစ်သောဘားအတွက်မေး, နှင့်ရိုးသားတဲ့ရလဒ်ကိုပုံမှန်အားဖြင့် panel ကိုအတိုဆုံးကျဆင်းသွားသောနေရာ၏တိကျတဲ့စာရင်းဖြစ်ပါသည် - သင်အဘယ်သူမျှမသင်ကိုယ်တိုင်စစ်ဆေးဖို့ရှိသည်လိမ့်မယ်အဘယ်သူမျှမယုံကြည်စိတ်ချရသောတောင်းဆိုမှုထက်ပိုပြီးတန်ဖိုးရှိပါတယ်.
ဒါဟာမဟုတ်တဲ့အခါမှာတည်ငြိမ်အဖြစ်အငြင်းပွားမှုတစ်ခုကိုဖြတ်သန်းခွင့်ပြုဖို့ငြင်းပယ်သောစက်တစ်ခုဖြစ်ပါတယ်, နှင့်သင်အတိအကျဘယ်အဆင့်ပျက်ကွက်ပြောပါတယ်.
ပျက်ကွက်သော ပုံစံကျ ထုတ်လုပ်မှုသည် အသုံးဝင်သော ထုတ်လုပ်မှုဖြစ်သည်
Lean သက်သေပြပိတ်ဆို့မည်မဟုတ်သောအခါ, သင်ကျန်ရစ်သောတိကျတဲ့ရည်မှန်းချက်ကိုရယူ. အလေ့အထ၌, ဤအလွန်အမင်းအမြဲတမ်းအဘယ်မှာရှိအငြင်းပွားမှုလက်-လှည့်ကွက်ခဲ့သည်နေရာမှာ spot ဖြစ်ပါတယ်။ — ခြေလှမ်းလူတိုင်းကဗျာဗားရှင်းဖတ်ရှုအတိတ်ကလက်ညှိုးထိုးခဲ့လိမ့်မယ်. ထိုရည်မှန်းချက်ကိုထိုအခါမည်သည့်အခန်းကဏ္ဍကိုတိုက်ခိုက်ရန်အကောင်းဆုံးနေရာချထားပေးသည်, အတူတူပင်စမ်းသပ်ခဲ့သည်အရာနှင့်အတူ, နှင့်အခြားဘာမှ. သူတို့က stuck နေကြတယ်အခါမော်ဒယ်များ thrash, ပြည့်စုံသောကုန်ကျစရိတ်တွင်သူတို့ကိုယ်သူတို့ပြန်ပြော; တစ်ဦးတိကျတဲ့မေးခွန်းကိုကျော်လွန်ခြင်းအစားပုံမှန်အားဖြင့် tokens များ၏တစ်စိတ်တစ်ပိုင်းအတွက် unblocks.
ကြာရှည်သောအလုပ်သည်ရှင်သန်
အားလုံးlemmaက panel ကိုတည်ထောင်သူ၏သက်သေအထောက်အထားနှင့်အတူမျှဝေဘဏ်စာရင်းထဲသို့သွား, ဒါကြောင့်ရလဒ်များကိုတစ်ကြိမ်ရေးသားထားပြီးမကြာခဏ re-derived နေကြတယ်, နှင့်အဆုံးသတ်အဆုံးသတ်မှတ်တမ်းတင်ထားသည်ဆိုလိုသည်မှာလူတိုင်းသူတို့ကိုပြန်သွားကြသည်.
ဒါဟာဘာအတွက်မဟုတ်ပါဘူး
ဤ site ကိုသင်္ချာအတွက်တည်ဆောက်ထားသည်, လောဂျစ်, သီအိုရီကွန်ပျူတာသိပ္ပံ, သီအိုရီရူပဗေဒနှင့်စီးပွားရေးသီအိုရီ - တစ်ခုကတောင်းဆိုချက်သက်သေအထောက်အထားအားဖြင့် settled နေရာမှာနယ်မြေများ. ဇီဝဗေဒအတွက် empirical မေးခွန်းများ, ဆေးဝါး, ဓာတုဗေဒသို့မဟုတ်လူမှုရေးသိပ္ပံသိပ္ပံများထုတ်လုပ်မပေး, သူတို့တွေ့ရှိချက်ထုတ်လုပ်, နှင့် formalization ၏အဘယ်သူမျှမပမာဏသူတို့ကိုဆုံးဖြတ်ပါလိမ့်မယ်။ ကျွန်တော်တို့ရဲ့အစ်မ site ကို referee.chat Lean အဆင့်မရှိဘဲတူညီ panel-and-referee လုပ်ငန်းစဉ်ကို runs, တိကျစွာထိုမေးခွန်းများအတွက်.
referee.chat — အလားတူစိတ်ကူး, empirical တောင်းဆိုချက်များအတွက်