Halmos ∎

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:

KuletsaZimene zikuchitikaKodi angapeze ∎?
lean Kuyesedwa kwa mtundu kudzera pa Mathlib. Kernel imavomereza mawu otsimikizira kapena ayi. Yes
sageSageMath amayenda izo; chiwonetsero chazithunzi chabwino ndi pinched kuti post.Si
gpPARI/GP imayendetsa izo.Si
z3Z3 amafuna mtundu: njira yofulumira kwambiri kukana chinachake.Si
pythonSandboxed 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

  1. Kuyankha moyenera. Masiku ambiri ali ndi maphunziro m'mawu awo pa zonse ndi chilichonse apa amafuna chilichonse.
  2. Kulemba maphunziro m'manja ndi $…$, kapena kusonyeza block ndi $$…$$. Imakhala ngati maphunziro a matepi amtundu wachikhalidwe; palibe chomwe chimachitika. Ndiko kungolemba. Onani imodzi
  3. Funsani makina. A fenced block tagged sage, gp, z3 kapena python ndi kuchitidwa pano ndi zotsatira zake kugwirizana ndi post wanu, verbatim. kuti ndi umboni, si umboni. Onani imodzi
  4. Kujambula ndi plot block (matplotlib, ndi plt ndi np otsimikiza), kapena kuzindikira ndondomeko ndi oeis: pezani integers ndi kuti amabwerera dzina, ngati ndi zodziwika bwino.
  5. Kusonyeza chinachake. A lean block 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 True ndi umboni, si umboni.
  • sorry, native_decide, a fresh axiom, unsafe ndi debug.skipKernelTC ndi 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.

Kugwirizana ndi kulankhulana.

Kulowa kuti alemba, kupulumutsa maganizo, ndi kutsatira anthu amene akupatsani mphamvu.

Kukhazikitsa akaunti · Kodi mwasiya mawu achinsinsi?

A dzina la wosuta ndi mawu achinsinsi ndi zonse zimene muyenera kuti ayambe.

Tumizani ife ndemanga

Tiuzeni zimene zinachitika kapena zimene munayembekezera. Tiwerenga meseji iliyonse.

Zikomo, ife tinapeza izo. Ngati inu anasiya imelo tidzayankha.