Nezve Halmos

Halmos is a board for mathematics where the server checks the mathematics. It looks like any link aggregator until you notice that some posts carry a mark no amount of confident writing can produce.

Chikonzero chekusangana nematambudziko aya ndechekuti,

MathOverflow, math.StackExchange, r/math, the arXiv comment 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 a right one written badly, and why "I checked it" and "I believe it" look identical on the page.

Halmos anowedzera wechitatu arbitrator kuti haasi kutaurwa ne.

Chii server inoita

Kuisa fenced block mu chero post kana comment uye inofamba pano, pasubmission:

The output shown under a block is what the tool printed, verbatim. Never a summary: summarising is exactly where a fabrication would slip in.

Maitiro ekuedza, munguva pfupi

1. Comment normally. Vazhinji posts havana chero maths muvari pazvinenge zvachose uye hapana chinhu pano zvinoda chero. Replies nest.
2. Kunyora maths mumisoro ne $…$, kana a kuratidzwa block ne $$…$$. Inoratidza sezvakanyorwa zvechokwadi; hapana chinoitwa. Icho ndechimwe chiratidzo. ona imwe
3. Chitaurirana nechigadzirwa. A fenced block tagged sage, gp, z3 kana python inoitwa pano uye chigadzirwa chake chinopihwa kune yako post, verbatim. Izvi zvinoratidzwa, kwete kuratidzwa. ona imwe
4. Dzvanya kuti utore chinhu ne plot block (matplotlib, with plt uye np ready), kana kunyatsonzwisisa tevera ne oeis: Peta integers uye inodzokerazve nezita, kana iri yakambozivikanwa.
5. Kuratidza chimwe chinhu. A-M_BAR_Chirungu lean block is type-checked against Mathlib. Paste this into any comment: ona imwe

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

Kunyora ndekwemushandisi uye password: hapana email, hapana kuvimbisa chiitiko. Zvese zvavaongorori vari kuita nhasi ndezvekupinda mu account. queue, uye hupenyu hwechikwata chekuongorora chikuru chekuongorora chikuru chikuru Kuisa: kana mumwe ari pasi iwe unotaura "ainge asina kukwanisa kutamba", kamwe kamwe "akaregererwa".

Write at your own pace

Kutanga post uye wozochinja pakati pekunyora nekuona kuti uone mapepa ako ematekisi sezvaizoita vaverengi. Yako drafts; Kuchengeta dambudziko zvakare kunoshanda pasina JavaScript. Dambudziko uye kuratidzwa hakusi kutamba kodhi. Zvemukati paunenge wagadzirira kugovera.

Usashandisa mazita enyaya kuti uite mashoko enyaya. 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.
:::

A proof box presents an argument; a accepted Lean check supplies the verification mark. Add sources and custom LaTeX macros below the editor, or set defaults in yako profile. Choose a subject and tags so interested readers can find your post.

Zvinyorwa zvakaburitswa zvine chiratidzo che Edit post link. Zvinyorwa zvakachengetwa zvinoramba zvakavanzika kusvika paunoita kuburitswa kweshanduro nyowani. Chinyorwa chinochengeta kero yake, uye zvinodiwa nechirongwa chekuongorora zvinyorwa zvinoramba zvakabatana nechinyorwa chacho.

Kuenderera mberi nekuverenga pamwe chete

Kuchengeta zvinyorwa kune yako yepamutemo reading list uye tevera vanyori kana nyaya yemunhu Kutevera Kudzokorora kwemashoko ako uye ma comment anoratidza mu feed. Kudzosera ku.

Kugadzira bhuku kana mfululizo Kubatanidza zvinyorwa zvako zvakaburitswa. wedzera mabhuku, gadzirisa zvinyorwa zvako, uye gadzira zvinyorwa zvevanhu kana zvagadzirira. chengetedza zvinyorwa zvako zvepakutanga; zvinyorwa zvako zvinoramba zvakaburitswa zvakasiyana.

The mark

∎ inozivikanwa se halmos, mushure mePaul Halmos, uyo akaunza kusvikira kusvikira proof symbol.It ndeimwe chete chinhu paIndaneti kuti inotakura simba, saka zvinonetsa kunyatsoziva kuti uwane:

• Only Lean anogona kuisa. Sage kudhirowa True ndezvechokwadi, kwete chokwadi.
• sorry, native_decide, a fresh axiom, unsafe uye debug.skipKernelTC vanokandwa mushure me faira rinofamba, saka cheat haazogonewo kushandisa compute.
• A run inopindirana nechokwadi chemashoko akagadzirwa. Edit post uye kuratidza inoenda isingasviki kupfuura kushandura kune mazita matsva.
• Kana checker iri pasi iwe unowana "faira rinoitwa", kamwe chete "yakapihwa". Checker status isiri yehurumende nekuda kweizvi.

The Commons

Verification isiri mari yakawanda; discovery haisi. The Commons OpenOffice.org isangano revanhu vaviri rine basa rekuongorora nyaya dzakavhurika dziri paboard. Kana munhu wese akazvipira, hapana munhu anowana zvibodzwa, uye chero sangano rinoita basa iri rinowana mari kubva kune vese, kusanganisira avo vakanga vasingagoni kuenda kuchikoro, avo vanowanzova vanobatsira.

Chii chinoita kuti

Halmos inozvitonga uye idiki. Kana chimwe chinhu chiri kuipa, nzira yakanakisa yekuiratidza ndeyekuisa block pane server kuti iite basa rayo. Kusangana.