Um Halmos
Halmos er borð fyrir stærðfræði þar sem miðlarinn athugar stærðfræðina. Það lítur út eins og hvaða tengil sem er þar til þú tekur eftir því að sum innlegg bera merki sem enginn magn af öruggu skrifun getur framleitt.
Vandamálið með öllum öðrum stærðfræði vettvangi
MathOverflow, math.StackExchange, r/math, arXiv athugasemdahlutarnir. Öll hafa þau einn réttlætisdómara: annað fólk, sem ræðir. Það virkar ótrúlega vel, og það er einnig ástæðan fyrir því að röng sönnun sem er skrifuð fljótt er í hærra sæti en rétt sönnun sem er skrifuð illa, og hvers vegna "ég athugaði það" og "ég trúi því" líta út eins á síðunni.
Halmos bætir við annarri dómara sem ekki er hægt að rífast við.
Hvað miðlarinn gerir í raun
Setja umkringd blokk í hvaða færslu eða athugasemd og það keyrir hér, á framlagningu:
| Blokk | Hvað gerist | Getur það fengið ∎? |
|---|---|---|
lean |
Tegund athuguð gegn Mathlib. Kjarninn samþykkir sannprófunarorð eða ekki. | Já |
sage | SageMath keyrir það; raunveruleg framleiðsla er fest við færsluna. | Nei |
gp | PARI/GP rekur ūađ. | Nei |
z3 | Z3 lítur út fyrir líkan: fljótlegasta leiðin til að hafna Eitthvađ. | Nei |
python | Sandboxed Python, úttak fylgir. | Nei |
Úttak sýnt undir blokk er það sem tólið prenta, bókstaflega. Aldrei samantekt: samantekt er nákvæmlega þar sem tilbúningur myndi renna inn.
Hvernig á að reyna það, í um eina mínútu
- Athugasemd venjulega. Flestar færslur hafa enga stærðfræði í þeim á öllum og ekkert hér krefst neins. Svar hreiður.
- Skrifa stærðfræði í línu með
$…$, eða skjáblokk með$$…$$. Það er gert eins og raunveruleg leturgerð stærðfræði; ekkert er framkvæmt. Það er bara táknmynd. Sjá einn - Spyrðu vélina. A gated block tagged
sage,gp,z3eðapythonÞað er framkvæmd hér og framleiðsla hennar fylgir innlegginu þínu, bókstaflega. Það er sönnunargögn, ekki sönnun. Sjá einn - Teikna eitthvað með
plotblokk (matplotlib, meðpltognptilbúinn), eða bera kennsl á röð meðoeis: líma heiltölur og það kemur aftur nefndur, ef það er þekkt. - Sannađu eitthvađ. A-M_BAR_Tyrkneska
leanblokk er gerð- athugað gegn Mathlib. Líma þetta í hvaða athugasemd: Sjá einn
```lean
import Mathlib
theorem two_add_two : 2 + 2 = 4 := by norm_num
```
Skráning er notandanafnið og lykilorðið: enginn tölvupóstur, engin staðfestingarskref.Allt sem skoðunarmenn eru að gera núna er á vefnum. biðröð, og lifandi ástand hvers skoðunarmanns er á staða síðu: Ef einn er niður þú ert sagt "gátu ekki keyrt", aldrei "höfðað".
Skrifaðu á eigin hraða
Byrjaðu færslu Og skipta á milli skrif og forskoðun til að sjá stærðfræði þína eins og lesendur munu. Drögin þín; Vista drög virkar líka án JavaScript. Drög og forskoðanir keyra aldrei kóða. Birta þegar þú ert tilbúinn að deila.
Notaðu fyrirsagnir til að byggja upp innihaldslista greinar. Valmyndin Setja inn bætir við skilgreiningum, setningum, sönnun, dæmum, töflum og tenglum. Til dæmis:
:::theorem Squares
For every real $x$, we have $x^2 \geq 0$.
:::
:::proof
Explain your argument here.
:::
Bættu við heimildum og sérsniðnum LaTeX-makróum undir ritlinum, eða stilltu sjálfgefnar stillingar í Sýna prófílinn þinnVeldu efni og merki svo áhugasamir lesendur geti fundið færsluna þína.
Birtar greinar hafa Breyta grein hlekk. Vistaðar breytingar eru einkamál þar til þú birtir uppfærsluna. Greinin heldur heimilisfanginu sínu og núverandi vélaskoðanir eru bundin við textann sem þær skoðuðu.
Haltu áfram að lesa saman
Vista innlegg á einka lestur lista og fylgja höfundum eða efni fyrir persónulega Eftirfarandi Svör við færslum þínum og athugasemdum birtast í Svarar þér.
Búa til bók eða röð Bættu við köflum, skipuleggðu röð þeirra og gerðu innihald þeirra opinbert þegar tilbúið. Einkasafn felur innihaldslistann sinn; innleggin í því eru áfram birt fyrir sig.
Merkiđ.
∎ Er kallað a halmos, eftir Paul Halmos, sem kynnti enda-af-sönnun tákn. Það er það eina á þessari síðu sem ber vald, svo það er vísvitandi erfitt að fá:
- Aðeins Lean getur sett það. Sage prentun
TrueÞetta er sönnunargögn, ekki sönnun. sorry,native_decide, fersktaxiom,unsafeogdebug.skipKernelTCeru hafnað fyrir Skráin keyrir, svo svikari getur ekki einu sinni eytt compute.- Hlaup er fest við nákvæmlega textann sem framleiddi það. Breyta færslu og merkið fer úr tísku frekar en að flytja til nýrra orða.
- Ef skákin er niður færðu "gat ekki keyrt", aldrei "hafnað". Staðsetning er opinber af þeirri ástæðu.
The Commons
Staðfesting er ódýr; uppgötvun er ekki. The Commons Hver sem er getur lagt sitt af mörkum, enginn á niðurstöðuna og hver einasta gerð sem hún fjármagnar er opinber, þar á meðal þær sem náðu ekki neinu fram, sem eru yfirleitt þær sem eru upplýsandi.
Hver rekur það
Halmos er sjálfstæður og lítill. Ef eitthvað hér er rangt, fljótlegasta leiðin til að sanna það er blokk miðlara sem hægt er að keyra. Hafðu samband.