တောင်းဆိုချက်ကိုပြောဆိုပါ။ kernel ကသက်သေပြနိုင်မလားဆိုတာကိုဆုံးဖြတ်သည်။

ပုံစံများ panel ကိုစာပေ, SageMath, PARI/GP နှင့် SMT solver နှင့်အတူသင်၏ပြဿနာကိုတိုက်ခိုက်, ထို့နောက် Lean 4 Mathlib အပေါ်အနိုင်ရ formalizes. Lean ရဲ့ kernel ကိုသို့မဟုတ်သက်သေခံလက်ခံသို့မဟုတ်မလုပ်ပါဘူး, နှင့်ယုံကြည်စိတ်ချရသောစာပေအရေအတွက်ကိုပြောင်းလဲသွား. ဒါဟာပျက်ကွက်တဲ့အခါသင်ကျန်ရစ်တဲ့တိကျတဲ့ရည်မှန်းချက်ရ, သောအများအားဖြင့်အဘယ်မှာရှိမတရားငြင်းခုံလက်-လှည့်ကွက်ခဲ့သည်.

ရည်ရွယ်ချက်

ပြုလုပ်ခဲ့သည်ဆိုလိုသည်မှာဘာအကြောင်းကိုတိကျတဲ့ဖြစ်ပါသည်. 'X ကိုမှန်ကန်ကြောင်းဆုံးဖြတ်ရန်, နှင့်သက်သေပြ' beats 'X ကိုအကြောင်းကိုပြောပါ'.

ရှင်းလင်းရန် လိုအပ်သော ဘက်ထရီ

Careful expert

What a competent professional in the field would accept as done and correct.

Publication standard

Would survive peer review: every claim sourced or derived, methods stated, limitations acknowle…

Formal proof

A complete deductive argument. Every step justified, every assumption stated, no appeals to pla…

Prize standard

The bar a Clay Millennium Prize submission would face: a complete, self-contained, gap-free pro…

Decision-grade

Enough evidence to act on commercially: options costed, risks named, recommendation justified.

Write my own

Describe your own standard.

အဆိုပါအစီရင်ခံစာကဤ bar ကို literally ကိုင်ထား. ဆု-level ကိုသက်သေပြချက်အတွက်မေးမြန်းခြင်းနှင့် panel ကိုတိုတောင်းသောကျဆင်းလာတဲ့အခါဒါဟာသင်ရှင်းလင်းစွာပြောလိမ့်မည်, ထက်အောင်ပွဲခံကြေညာ.

ပင်မမျက်နှာပြင်

ပိုပြီးထိုင်ခုံများပိုပြီး angles အဓိပ္ပါယ်, နှင့် round တစ်ဦးလျှင်ပိုမိုကုန်ကျစရိတ်.

ဆုံးဖြတ်သူ

စံချိန်စံညွှန်းများအပေါ်စည်းမျဉ်းစည်းကမ်းများနှင့်သက်သေအထောက်အထားအားလုံးအပိုင်းအစ re-စစ်ဆေး. သင့်ရဲ့အခိုင်အမာဆုံးမော်ဒယ်တန်ဖိုးထား.

စက်ဝိုင်းများ

ကုန်ကျစရိတ် ကနဦး

ရိုက်နှက်ခြင်းဖြင့် ပွဲကို ရပ်တန့်စေသည်။ အရာရာတိုင်း ဆုံးရှုံးသွားသည်။

မြင်နိုင်စွမ်း

ပြီးဆုံးချိန်တွင် ထုတ်ဝေပါ

ပွဲစတင်ရန် မှတ်ပုံတင်ပါ

အသစ်အကောင့်များစတင်ခရက်ဒစ်ရ, အမှန်တကယ်ပွဲအတွက်လုံလောက်.

သက်သေခံချက်ကို ငြင်းဆိုလို့မရဘူး

Mathlib အမျိုးအစား-စစ်ဆေးခြင်းနှင့်အတူ Lean 4 နောက်ဆုံးထုတ်ပြန်ချက်, နှင့် sorry, native_decide သို့မဟုတ်အသစ် axiom အပေါ်လှဲချကြောင်းသက်သေပြချက်ထက်စာရင်းပြုစုခံရဖို့ငြင်းပယ်ခံရ. ဒါဟာဘေးတွင်: SageMath, PARI/GP, Z3, CVC5 နှင့် OEIS, ဒါကြောင့်တစ်ဦးဆောက်လုပ်ရေးကွန်ပျူတာနှင့်လူတိုင်းကအကြောင်းအရာတစ်ခုခုကိုသက်သေပြဖို့ကြိုးစားမတိုင်မီအမည်မသိနိုင်ပါတယ်.

ပျက်ကွက်သက်သေပြချက်တစ်ခုရှာဖွေတွေ့ရှိမှုဖြစ်ပါသည်

formalization ပျက်ကွက်တဲ့အခါ, ရည်မှန်းချက် Lean မပိတ်နိုင်ခဲ့သည်မည်သည့်နေရာကိုတိုက်ခိုက်ရန်အကောင်းဆုံးနေရာချထားပေးသည်: မျှသာထိုရည်မှန်းချက်, တစ်ခုလုံးသမိုင်းမဟုတ်. ငြင်းပယ်သက်သေအထောက်အထားအတိအကျကွာခြားချက်နာမကိုခေါ်, အများဆုံးမတရားသောငြင်းခုံမှုအစဉ်အမြဲလုပ်ထက်ပိုပြီးဖြစ်ပါတယ်.

ဘာမှနှစ်ကြိမ်သက်သေပြသည်

အားလုံးlemmaက panel ကိုတည်ထောင်သည်သူ၏သက်သေအထောက်အထားနှင့်အတူမျှဝေဘဏ်စာရင်းထဲသို့သွား, ဒါကြောင့်ဒါဟာမကြာခဏ re-derived နှင့်အဆုံးသတ်အဆုံးသတ်မကြာခဏ retry နေကြတယ်.