Halmos အကြောင်း

Halmos server ကိုသင်္ချာစစ်ဆေးနေရာတွင်သင်္ချာအတွက်ဘုတ်အဖွဲ့တစ်ခုဖြစ်ပါသည်. သင်အချို့ posts များကိုထုတ်လုပ်နိုင်မည်မဟုတ်ကြောင်းသေချာရေးသားခြင်း၏အရေအတွက်မရှိအမှတ်ကိုဆောင်ကြဉ်းကြောင်းသတိပြုမိသည်အထိမည်သည့် link ကို aggregator ကဲ့သို့ကြည့်ရှု.

အခြားတိုင်းသင်္ချာဖိုရမ်နှင့်အတူပြဿနာ

MathOverflow, math.StackExchange, r / math, the arXiv comment sections. သူတို့အားလုံးမှန်ကန်မှု၏အတိအကျတစ်ခု arbitrator ရှိပါတယ်: အခြားလူများ, ငြင်းခုံ. ဤသည်အံ့သြဖွယ်ကောင်းစွာအလုပ်လုပ်တယ်, နှင့်လည်းအဘယ်ကြောင့်တစ်ဦးမှားယွင်းသောသက်သေခံစာရေးသား fluently မကောင်းစွာရေးသားတစ်ဦးမှန်ကန်သောတစ်ဦးကို outranks ဖြစ်ပါသည်, နှင့်အဘယ်ကြောင့် "ငါကစစ်ဆေး" နှင့် "ငါယုံကြည်" စာမျက်နှာပေါ်တွင်တူညီသောကြည့်ရှု.

Halmos အတူငြင်းခုံနိုင်ခြင်းမရှိသောဒုတိယ arbitrator ထည့်သွင်းသည်။

ဆာဗာက တကယ်လုပ်နေတာ

မည်သည့် post သို့မဟုတ်မှတ်ချက်တွင်ပင် ပတ်ပတ်လည်ဘလော့ဂ်တစ်ခု ထည့်သွင်းပြီး တင်သွင်းမှုတွင် ဤနေရာတွင် လည်ပတ်ပါ:

block တစ်ခုအောက်တွင်ပြသ output ကို tool ကိုပုံနှိပ်ဘာဖြစ်ပါသည်, လုံးဝ. တစ်ဦး summary မကြာခဏ: summarising တိကျစွာတစ်ဦး fabrication အတွင်းသို့ slip လိမ့်မယ်နေရာမှာဖြစ်ပါတယ်.

ဘယ်လိုကြိုးစားကြည့်ပါ, တစ်မိနစ်အတွင်း

1. မှတ်ချက် ပုံမှန်အတိုင်း။ အများစု posts များသူတို့ကိုအားလုံးနှင့်ဘာမှဒီမှာလိုအပ်သည်မည်သည့်အတွက်သင်္ချာမရှိ.
2. သင်္ချာများကို လိုင်းအတွင်းရေးပါ အတူ $…$, သို့မဟုတ်အတူပြသဘုတ်အဖွဲ့ $$…$$. တကယ့် စာလုံးပေါင်း သင်္ချာအဖြစ် ပေးပို့ပါ၊ ဘာမှ မလုပ်ပါနဲ့။ မှတ်ချက်တစ်ခုပဲ ပေးပို့ပါ တစ်ခုတွေ့မြင်
3. စက်ကိုမေးပါ။ တံဆိပ်တုံး တပ်ထားသော ပတ်ပတ်လည် အုပ်စု sage, gp, z3 သို့မဟုတ် python ဒီမှာ executed ဖြစ်ပြီး၎င်း၏ output ကိုသင်၏ post ကိုချိတ်ဆက်, လုံးဝ. ဒါဟာသက်သေအထောက်အထားဖြစ်ပါတယ်, သက်သေအထောက်အထားမဟုတ်. တစ်ခုတွေ့မြင်
4. တစ်ခုခုဆွဲပါ အတူ plot block ကို (matplotlib, အတူ plt နှင့် np အဆင်သင့်), သို့မဟုတ်အတူ sequence ကိုခွဲခြားသတ်မှတ် oeis: အားလုံးနံပါတ်များကို paste နှင့်၎င်းသည်သိရှိပါကအမည်ပေးပြန်လာသည်.
5. တစ်ခုခုကို သက်သေပြပါ။ အင်္ဂလိပ် lean block ကို Mathlib ကိုဆန့်ကျင် type-စစ်ဆေးသည်. မည်သည့်အကြံပြုချက်သို့ဤ paste: တစ်ခုတွေ့မြင်

```lean
import Mathlib
theorem two_add_two : 2 + 2 = 4 := by norm_num
```

တက်လက်မှတ်ရေးထိုး username ကိုနှင့် password ကိုဖြစ်ပါသည်: အီးမေးလ်မရှိ, မည်သည့်အတည်ပြုခြေလှမ်း. အားလုံး checkers အခုတော့လုပ်နေတာအရာအားလုံးအပေါ်ဖြစ်ပါတယ် တန်းစီ, နှင့်တစ်ဦးချင်းစီ checker ရဲ့အသက်ရှင်နေထိုင်နိုင်ငံအပေါ်ဖြစ်ပါသည် အခြေအနေစာမျက်နှာ: တစ်ခုခုကိုအောက်မှာသင်ပြောပါတယ်လျှင် "မ Run နိုင်ခဲ့", မ "ငြင်းပယ်" ။

သင်၏ကိုယ်ပိုင်အရှိန်ဖြင့်ရေးပါ

ပို့စ်တစ်ခုစတင်ပါ ဖတ်ရှုသူအဖြစ်သင်၏သင်္ချာကြည့်ရှုရန်စာရေးခြင်းနှင့် preview ကြား switch ကို. ပြောင်းလဲမှုများကိုအလိုအလျောက် save သင့်အစီရင်ခံစာများ; Save draft also works without JavaScript. drafts and previews never run code. သင်မျှဝေဖို့အဆင်သင့်ဖြစ်တဲ့အခါ publish.

ဆောင်းပါး၏အကြောင်းအရာစာရင်းကိုတည်ဆောက်ရန်ခေါင်းစဉ်များကိုအသုံးပြုပါ။ Insert menu ကိုအဓိပ္ပာယ်ဖွင့်ဆိုချက်, theorems, သက်သေပြချက်, ဥပမာများ, စားပွဲ, နှင့်လင့်များထည့်သွင်းသည်။ ဥပမာအားဖြင့်:

:::theorem Squares
For every real $x$, we have $x^2 \geq 0$.
:::

:::proof
Explain your argument here.
:::

သက်သေပြ box ကိုတစ်ဦးအငြင်းပွားမှုတင်ပြ; တစ်ခုလက်ခံရရှိ Lean စစ်ဆေးခြင်းစစ်ဆေးခြင်းအမှတ်ပေးပို့. ရင်းမြစ်များနှင့်အထူးပြု LaTeX macros editor ကိုအောက်တွင်ထည့်သွင်း, သို့မဟုတ် defaults ကို setting သင်၏ profile ကို. အကြောင်းအရာနှင့် tags များကိုရွေးချယ်ပါ, ထိုသို့စိတ်ဝင်စားဖတ်ရှုသူသင်၏ post ကိုရှာတွေ့နိုင်ပါတယ်.

ထုတ်ဝေ posts များ post ကို Edit link ကိုရှိပါတယ်. Saved တည်းဖြတ်မှုများသင်အသစ်တစ်ခုကိုထုတ်ဝေမတိုင်မီပုဂ္ဂလိကတည်ရှိနေ. ဆောင်းပါးသည်၎င်း၏လိပ်စာကိုထိန်းသိမ်းထား, နှင့်လက်ရှိစက်စစ်ဆေးမှုများသူတို့စစ်ဆေးခဲ့သောစာသားကိုချိတ်ဆက်နေထိုင်.

အတူတူဖတ်ရှုရန်ဆက်လက်

သင့်ရဲ့ပုဂ္ဂလိကဖတ်ရှုစာရင်းအတွက် posts တွေကို Save ပြီးပုဂ္ဂိုလ်ရေးအတွက်စာရေးဆရာများသို့မဟုတ်အကြောင်းအရာများကိုလိုက်နာ လိုက်နာခြင်း feed ကို. သင့်ရဲ့ posts များကိုနှင့်အကြံပြုချက်များကိုတုံ့ပြန်ချက်ထဲမှာပေါ်လာ သင့်ကိုပြန်ကြားချက်.

စာအုပ် သို့မဟုတ် စီးရီးတစ်ခု ဖန်တီးပါ သင့်ရဲ့ထုတ်ဝေ posts များကိုချိတ်ဆက်ရန်. အခန်းပေါင်း Add, သူတို့ရဲ့အမိန့်ကိုစီစဉ်, နှင့်အဆင်သင့်ဖြစ်တဲ့အခါ contents များကိုပြည်သူ့လုပ်. တစ်ဦးပုဂ္ဂလိက collection ကို၎င်း၏ contents စာရင်းကိုပိတ်ထား; ၎င်း၏ posts များကိုတစ်ဦးချင်းစီထုတ်ဝေနေဆဲ.

အမှတ်

∎ ဟုခေါ်သည် halmos, ပေါလု Halmos နောက်ပိုင်း, သက်သေပြခြင်း၏အဆုံး-၏သင်္ကေတကိုမိတ်ဆက်သူ. ဒါဟာအာဏာဆောင်သောဤ site ပေါ်တွင်တစ်ခုတည်းသောအရာဖြစ်ပါသည်, ဒါကြောင့်ဒါဟာရဖို့စိတ်ကူးယဉ်ခက်ခဲဖြစ်ပါတယ်:

• တစ်ခုတည်း Lean သတ်မှတ်နိုင်ပါတယ်. Sage ပုံနှိပ် True သက်သေခံချက်ဖြစ်ပါတယ်, သက်သေခံချက်မဟုတ်.
• sorry, native_decide, အသစ် axiom, unsafe နှင့် debug.skipKernelTC ငြင်းပယ်ခံရသည် ရှေ့မှာ file ကို runs, ဒါကြောင့်တစ်ဦး cheat ပင် compute ကိုသုံးစွဲနိုင်ခြင်းမရှိပါ.
• A run is pinned to the exact text that produced it. ဤ post ကိုတည်းဖြတ်ခြင်းနှင့်အမှတ်အသားအသစ်သောစကားလုံးများသို့လွှဲပြောင်းထက်ပိုပြီးအဟောင်းသွား.
• တစ်ဦးစစ်ဆေးခြင်းသင်ရဖို့အောက်မှာဖြစ်ပါတယ်လျှင် "မဖွင့်နိုင်ဘူး", ဘယ်တော့မှ "ငြင်းပယ်". အခြေအနေစစ်ဆေး အကြောင်းပြချက်အတွက် အများပြည်သူဖြစ်ပါသည်.

အများသုံး

သက်သေပြချက်သည် ဈေးပေါသည်၊ တွေ့ရှိချက်သည် မဟုတ်ပါ။ အများသုံး ဤဘုတ်အဖွဲ့အထက်မဲပေးခဲ့သည်သောပွင့်လင်းပြဿနာများအပေါ် grinds သော compute ၏မျှဝေ pool တစ်ခုဖြစ်ပါသည်. မည်သူမဆိုဒါကိုထောက်ပံ့နိုင်ပါတယ်, ဘယ်သူမှရလဒ်ကိုပိုင်ဆိုင်, နှင့်တိုင်း run ရန်ပုံငွေများပြည်သူ့ဖြစ်ပါသည်, ဘယ်နေရာမှာမှမရခဲ့သောသူတို့အပါအဝင်, အများအားဖြင့်သတင်းအချက်အလက်များသောသူတို့ဖြစ်ကြသည်.

ဘယ်သူ့မှမောင်းနှင်

Halmos လွတ်လပ်ပြီးသေးငယ်တဲ့ဖြစ်ပါသည်. ဒီမှာတစ်ခုခုမှားနေတယ်ဆိုရင်, သက်သေပြဖို့အမြန်ဆုံးနည်းလမ်းက server ကို run နိုင်ပါတယ် block တစ်ခုဖြစ်ပါတယ်. ဆက်သွယ်ပါ.