Za Halmos
Halmos ndi board kwa maphunziro kumene server amayesa maphunziro. Zikuwoneka ngati aliyense kugwirizana aggregator mpaka inu muona kuti ena posts kunyamula mfundo palibe ndalama yodalirika kulemba angachititse.
Mkangano ndi aliyense wina matebulo a mathematics
MathOverflow, math.StackExchange, r/math, arXiv comments sections. All of them have exactly one arbiter of correctness: other people, arguing. That works remarkably well, and it is also why a wrong proof written fluently overranks one right written badly, and why "I checked it" and "I believe it" look identical on the page.
Halmos awonjezera 2nd arbitrator kuti sizingatheke kugawidwa ndi.
Kodi server akuchita
Pogwiritsa ntchito block blocked mu chilichonse kapena uthenga wa ndemanga ndipo imayenda pano, pa kutumiza:
| Kuletsa | Zimene zikuchitika | Kodi angapeze ∎? |
|---|---|---|
lean |
Kuyesedwa kwa mtundu kudzera pa Mathlib. Kernel imavomereza mawu otsimikizira kapena ayi. | Yes |
sage | SageMath amayenda izo; chiwonetsero chazithunzi chabwino ndi pinched kuti post. | Si |
gp | PARI/GP imayendetsa izo. | Si |
z3 | Z3 amafuna mtundu: njira yofulumira kwambiri kukana chinachake. | Si |
python | Sandboxed Python, kutulutsa kuphatikizidwa. | Si |
Kutulutsa kusonyeza pansi pa block ndi zimene chida anasindikiza, verbatim. Kamodzinso m'munsimu: m'munsimu ndi moyenera pamene kupanga angagwiritse ntchito.
Momwe mungayesere, m'maola angapo
- Kuyankha moyenera. Masiku ambiri ali ndi maphunziro m'mawu awo pa zonse ndi chilichonse apa amafuna chilichonse.
- Kulemba maphunziro m'manja ndi
$…$, kapena kusonyeza block ndi$$…$$. Imakhala ngati maphunziro a matepi amtundu wachikhalidwe; palibe chomwe chimachitika. Ndiko kungolemba. Onani imodzi - Funsani makina. A fenced block tagged
sage,gp,z3kapenapythonndi kuchitidwa pano ndi zotsatira zake kugwirizana ndi post wanu, verbatim. kuti ndi umboni, si umboni. Onani imodzi - Kujambula ndi
plotblock (matplotlib, ndipltndinpotsimikiza), kapena kuzindikira ndondomeko ndioeis: pezani integers ndi kuti amabwerera dzina, ngati ndi zodziwika bwino. - Kusonyeza chinachake. A
leanblock ndi type-checked kudzera Mathlib. Pezani izi mu chilichonse ndemanga: Onani imodzi
```lean
import Mathlib
theorem two_add_two : 2 + 2 = 4 := by norm_num
```
Kulembetsa ndi dzina la ogwiritsa ntchito ndi mawu achinsinsi: palibe imelo, palibe gawo lotsimikizira.Zosefera zonse zomwe zikuchita pano ndizo pa intaneti. mnda, ndi moyo wa dziko la aliyense woyang'anira ndi pa status page: ngati wina ndi pansi inu ndinu kufotokoza "kukhoza kuyendetsa", nthawi zonse "kulephera".
Kulemba pa nthawi yanu
Kuyamba nkhani ndi kusintha pakati pa kulemba ndi preview kuona maphunziro anu monga owerenga adzachita. Ma drafts anu; Kusunga ma draft kumagwira ntchito popanda JavaScript. Ma draft ndi ma previews sagwira ntchito. Kufalitsa pamene muli okondwa kugawana.
Use headings to build an article's contents list. The Insert menu adds definitions, theorems, proofs, examples, tables, and links. For example:
:::theorem Squares
For every real $x$, we have $x^2 \geq 0$.
:::
:::proof
Explain your argument here.
:::
Kuwonjezera malemba ndi zosiyanasiyana LaTeX macros pansi pa wopanga, kapena kukhazikitsa defaults mu Kusintha kwa profile yanu. Sankhani nkhani ndi tags kuti owerenga ofuna angapeze wanu post.
Zolemba zosindikizidwa zili ndi chingwe chosintha zolemba. Zolemba zosindikizidwa zimakhala zachikhalidwe mpaka mutafalitsa zosinthazo. Nkhaniyo imasunga adiresi yake, ndipo zoyeserera za makina zomwe zilipo zimakhala zogwirizana ndi malemba omwe adayeserera.
Kutsatira kuphunzira limodzi
Kusunga malemba pamnda wanu wapadera wowerenga ndi kutsatira olemba kapena maphunziro kwa Kutsatira Mayankho a zolemba zanu ndi ndemanga zimawonekera mu Mayankho kwa inu.
Kukhazikitsa buku kapena mnda Kuphatikizapo mabuku, kupangira ndondomeko yawo, ndi kuchititsa zomwe zilipo kuti zikhale za anthu onse pamene zikutha. Kusonkhanitsa kwapadera kumachotsa zomwe zilipo; zomwe zilipo zimakhala zofalitsa zokha.
Mtundu
∎ amatchedwa halmos, pambuyo Paul Halmos, amene anayambitsa kumapeto-of-proof chizindikiro. Ndi chinthu chokha pa webusaitiyi kuti amabweretsa ufulu, kotero ndi zozizwitsa zovuta kupeza:
- Koma Lean angaipange. Sage kusindikiza
Truendi umboni, si umboni. sorry,native_decide, a freshaxiom,unsafendidebug.skipKernelTCndi zosavomerezeka pambuyo fayilo imayenda, kotero cheat singathenso kulipira compute.- A kunyamula ndi pined kuti mawu osati kuti anapanga izo. Sinthani post ndi mfundo imakhala kale kuposa kutengerapo kwa mawu atsopano.
- Ngati checker ndi pansi mudzakhala "sanathe kuyendetsa", nthawi zonse "adalephera". Checker status ndi anthu chifukwa cha izo.
Ma Commons
Kuyesa ndi yosavuta; kuzindikira si. Ma Commons Wikidata ndi malo ogawana a compute omwe amapanga mayankho a mavuto otsegulidwa omwe board iyi yasankha. Womwe aliwonse angathandize pa izi, palibe amene ali ndi zotsatira zake, ndipo ndalama zonse zomwe zimagulitsidwa ndi anthu, kuphatikizapo zomwe sizipezeka, zomwe nthawi zambiri zimapezeka.
Kodi ndi ndani amene amayendetsa
Halmos ndi wodziyimira pawokha ndi wamng'ono. Ngati chinachake pano ndi zoipa, njira yofulumira kusonyeza kuti ndi block server angagwiritse ntchito. Kulumikizana.