Ku saabsan Halmos

Halmos waa guddiga xisaabta halkaas oo server xisaabta tijaabiyo. Waxay u egtahay sida xiriir kasta oo aggregator ilaa aad ogaato in qaar ka mid ah posts qaado calaamad aan waxba oo lacag ah oo qoraalka kalsooni ku abuuri kartaa.

dhibaatada la mid ah forum kasta oo kale oo xisaabta ah

MathOverflow, math.StackExchange, r/math, arXiv comment sections. Dhammaantood waxay leeyihiin mid sax ah oo sax ah: dadka kale, doodda. Taasi waa wax aad u fiican, iyo waa sababta oo ah caddayn qalad ah oo la qoray si fiican u qoray mid sax ah oo si xun loo qoray, iyo sababta "waxaan u tijaabiyey" iyo "waxaan u aaminsanahay" in ay u muuqdaan mid la mid ah bogga.

Halmos ku daray garsoore labaad oo aan la isku raacsan yahay.

Waxa server dhab ahaantii sameeyaa

Ku shub block la xiray in post kasta ama faallo iyo waxa uu ku socdaa halkan, on gudbinta:

Wax soo saarka hoos block waxaa lagu muujiyey waxa qalabka daabacay, literal. marnaba warbixin: warbixin waa si toos ah meesha wax soo saarka ku dhici lahaa.

Sida loo isku dayo, in daqiiqo ku saabsan

1. Faallo caadi ah. Post badani ma leeyihiin xisaabta iyaga ku jira oo dhan iyo waxba halkan u baahan yahay mid kasta. Jawaabaha tuubbada.
2. Ku qor xisaabta xagga hoose la $…$, ama blokka bandhigga la $$…$$. Waxay u muuqataa sida tifaftiraha dhabta ah ee xisaabta; waxba ma la fulin. Waa kaliya calaamadeynta. ka eeg mid
3. weydii mashiinka. Blokka la calaamadiyey ee la xiray sage, gp, z3 ama python waa la fuliyay halkan iyo natiijada la xidhiidha post aad, qoraalka. Taasi waa caddayn, ma caddayn. ka eeg mid
4. Wax ka riix la plot block (matplotlib, la plt iyo np diyaar), ama aqoonsado silsilad la oeis: paste inta badan iyo waxaa dib u yimaado magaciisa, haddii ay la yaqaan.
5. Xusuusnow wax. A-M_BAR_Af-Carabi lean block waa nooc-ka-eegista ka dhanka ah Mathlib. Ku dheji this in wax walba oo faahfaahin: ka eeg mid

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

Soo diiwaangelinta waa username iyo password: email ma jiro, tallaabo xaqiijin ma jiro. Wax kasta oo checkers ay sameynayaan hadda waa on kala guurka, iyo xaaladda nool ee checker kasta oo ah waa ku status page: haddii mid ka mid ah hoos ayaad ku odhan "ma dhicin", marnaba "la diiday".

Ku qor xawaarahaaga

Bilaw qoraal iyo u beddelaan u dhexeeya qorista iyo hordhaca si aad u aragto xisaabtaada sida akhristaha. Qoraalkaaga; Save draft sidoo kale shaqeysaa aan JavaScript. Drafts iyo hordhaca ma run code. daabac marka aad diyaar u tahay in ay qaybsadaan.

Ku isticmaal magacyada si aad u dhisto liiska waxyaabaha maqaalka. Liiska ku dheji waxa uu ku darayaa macnaheedu, theorems, proofs, tusaale, tabo, iyo xiriirada. tusaale ahaan:

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

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

A box caddayn soo bandhiga argument; a aqbalay tijaabada Lean bixisaa calaamadda xaqiijinta. Ku dar macluumaadka iyo macruufka LaTeX custom hoos editor, ama ku abuuraan defaults in profil-kaaga. Dooro mawduuc iyo tags si akhristaha xiiseynayaa ay ka heli karaan post aad.

Qoraallada la daabacay waxaa jira Edit post link. Edits kaydinta ku sii joogaan gaar ah ilaa aad daabacdo cusbooneysiinta. Qoraalka ku haystaa cinwaanka, iyo tijaabooyinka mashiinka jira ku sii joogaan ku xidhan qoraalka ay tijaabiyeen.

Ku sii akhrin la socda

kaydinta posts in aad akhrinta liiska gaarka ah iyo raacaan qorayaal ama mawduucyada si ay u Ka dib feed. jawaabaha aad posts iyo faallooyinka ka muuqdaan Jawaab kuugu.

abuuro buug ama silsilad Add chapters, u diyaariyaan amarkooda, iyo in ay contents dadweynaha marka ay diyaar u yihiin. A ururinta gaar ah qarin contents list; posts ay sii wadaan in ay soo saaraan qof walba.

Calaamada

∎ waxaa loo yaqaan halmos, ka dib markii Paul Halmos, oo soo bandhigay calaamadda dhamaadka-of-muujintii. Waa waxa kaliya ee goobta in ay qaaddo awoodda, sidaas darteed waa si gooni ah u adag in la helo:

• Lean kaliya ayaa ku dari kara. Sage daabacaadda True waa caddayn, ma aha caddayn.
• sorry, native_decide, cusub axiom, unsafe iyo debug.skipKernelTC waa la diiday ka hor faylka socda, sidaas daraaddeed cheat ma awoodo in ay ku bixiyaan xisaabta.
• A socdaal waa la xiray in qoraalka saxda ah ee uu soo saaray. Edit post iyo calaamadda u socdaa oo aan la soo celin ka badan in ay ku wareejiyaan ereyga cusub.
• Haddii checker waa hoos aad ka heli "ma awoodin inaad fuliso", marnaba "la diiday". Ka hubi xaaladda waa dadweynaha sababtaas awgeed.

Shabakadda

Verification waa qiimo jaban; ogaado ma aha. Shabakadda waa biyo-dhaca qaybsan ee xisaabinta in ay ku qalajiso dhibaatooyinka furan ee guddigaas uu codeeyay kor. Qof kastaa wuxuu ka qayb qaadan karaa, qofna ma laha natiijada, iyo run kasta oo ay lacagaha waa dadweynaha, oo ay ku jiraan kuwa aan meelna ka helin, kuwaas oo caadi ahaan kuwa warbixinnada ah.

Cidda uu ka socdaa

Halmos waa madaxbannaan yahay oo yar. Haddii wax halkan waa qalad, habka ugu dhaqsaha badan ee lagu muujiyo waa block server ka run kartaa. La xiriir.