Ngo-Halmosh
Halmos yibhodi le-matematics lapho umhlinzeki ebheka khona i-matematics. Kubukeka sengathi yinoma iyiphi i-link aggregator kuze kube uqaphele ukuthi ezinye izi-posts ziphethe i-mark akukho inani lokubhalela okuthembekile okuzokhiqizwa.
Inkinga ngazo zonke ezinye izingqungquthela ze-mathematics
MathOverflow, math.StackExchange, r/math, i-arXiv comment sections. Zonke zinomlingani ofanayo wokuhle: abanye abantu, bekhuluma. Lokhu kusebenza kahle kakhulu, futhi kuyisizathu sokuthi isizathu esibi esibhalwe ngokugcwele sihamba phambili kusinye esibhalwe kahle, futhi kungani "Ngiyibheka" ne "Ngiyikholelwa" zibukeka zifana kwikhasi.
Halmos ifaka isilinganisi sesibili esingaba khona ukuxoxwa ngaso.
Igama leseva
Faka i-block ehlotshiswe nganoma iyiphi incwadi noma umlayezo futhi isebenza lapha, uma ifakwe:
| I-block | Yini ekwenzeka | Ingabe ithola imali ∎? |
|---|---|---|
lean |
Uhlobo oluhlolwe ku-Mathlib. I-kernel ivuma amagama obufakazi noma ayisebenzi. | Yebo |
sage | I-SageMath iqhuba; okuqukethwe okusemthethweni kufakwe ku-post. | Akukho |
gp | I-PARI/GP isebenza kuyo. | Akukho |
z3 | Z3 ibheka imodeli: indlela ekhawulezayo yoku chaza into. | Akukho |
python | I-Python efakwe i-sandbox, isingeniso sixhunywe. | Akukho |
I-output ebonisa ngezansi kwe-block yilokho okuphrintiwe yithuluzi, ngokusho kwegama. Ungaze ubeke isiqubulo: isiqubulo siyilapho ukwenziwa kuzoba khona.
Indlela yokuzama, cishe imizuzu embalwa
- Umbono ojwayelekile. Amanye ama-posts angeke abe nama-maths kuwo wonke umuntu futhi akukho okudingayo lapha.
- Bhala i-mathematics engezansi nge
$…$, noma iblokhi yokukhombisa ene$$…$$. Ibonisa njengezibalo zesizinda se-typeset; akukho okuqhutshwayo. Kuyinto nje inkomba. bona eyodwa - Buza imishini. Ibloki elisha eliphawulwe
sage,gp,z3nomapythonisebenza lapha futhi ikhishwa kwayo lixhunywe ku-post yakho, ngokucacile. Lokhu kuyiqiniso, hhayi bufakazi. bona eyodwa - Dweba into ethile nge
plotblock (matplotlib, withpltfuthinpukulungele), noma ukhomba umkhondo ngeoeis: chofoza inani eliphelele futhi lizobuyela ngegama, uma liziwa. - Ubufakazi bokuthi kukhona okuthile. A-M_BAR_Isi-Italian
leani-block ihlolwe uhlobo-lokuhlola ku-Mathlib. Chofoza lokhu kuwo wonke umlayezo: bona eyodwa
```lean
import Mathlib
theorem two_add_two : 2 + 2 = 4 := by norm_num
```
Ukubhalisa kudinga igama lomsebenzisi nephasiwedi: akukho i-imeyili, akukho inyathelo lokuqinisekiswa. Konke okuzokwenziwa yilabo abahlolayo manje ku- ifolomu, futhi ngayinye checker's live state is on the ikhasi lesimo: uma enye iphansi utshela ukuthi "akufanele uphume", akufanele "ukwehliwe".
Bhala ngezinga lakho
Qala incwadi enemingwane futhi ushintshe phakathi kokubhala nokubheka kuqala ukubona i-mathematics yakho njengoba abafundi bazo. Ushintsho lugcinwa ngokuzenzakalela Amadrafti akho; Gcina i-drawing isebenza ngaphandle kwe-JavaScript. I-drawing nemboniso-sithombe azisebenzisi ikhowudi. Yazisa uma ukulungele ukuhlanganisa.
Sebenzisa izihloko ukwakha uhlu lwezinto eziqukethwe isihloko. Imenyu Yokufaka ifaka izichazamazwi, izimiso, iziqinisekiso, izibonelo, izibonelo, amathebula, namakhonkco. Umzekelo:
:::theorem Squares
For every real $x$, we have $x^2 \geq 0$.
:::
:::proof
Explain your argument here.
:::
Ibhokisi lobufakazi libonisa isiphakamiso; ukuhlolwa okuvunyelwe kwe-Lean kuhlinzeka ngephawu lokuqinisekiswa. Engeza amakhompiyutha nama-macros we-LaTeX ajwayelekile ngaphansi komhleli, noma hlela izilungiselelo ezizenzakalelayo iprofayili yakho. Khetha isiqephu kanye namathegi ukuze abafundi abafunayo bakwazi ukuthola incwadi yakho.
Izihloko ezishicilelwe zine-Edit post link. Izihloko ezigcinwe zihlala zifihlakele kuze kube ushicilela ukuhlaziywa. Isihloko sigcina ikheli layo, futhi ukuhlolwa kwemishini okukhona kuhlala kuxhunywe kubhalo okuhlolwa kwayo.
Qhubeka ufunda ndawonye
Gcina izithunywa kuluhlu lwakho lokufundela olufihlakele futhi ulandele ababhali noma izihloko eziphathelene nawe Okulandelayo feed. Izinphendulo ku posts yakho kanye nokuphawula ubonakala Uphendulela kuwe.
Dala incwadi noma isiqephu ukuxhuma izixhumanisi zakho ezishicilelwe. Engeza amasigaba, hlela ukulandelana kwabo, futhi wenze izixhumanisi ziyimfihlo uma zilungile. Uhlelo olufihlakele lufihla uhlu lwezixhumanisi; izixhumanisi zayo zihlala zishicilelwe ngazo zonke.
Iphawu
∎ ibizwa nge halmos, ngemuva kukaPaul Halmos, owasungula isibonakaliso sokuphela-sobufakazi. Kulokhu kuyinto eyodwa kule ndawo ephethe igunya, ngakho-ke kunzima ukufinyelela:
- Lean kuphela ongakwazi ukuhlela lokhu. Sage printing
Trueikhombisa, hhayi ikhombisa. sorry,native_decide, i-freshaxiom,unsafefuthidebug.skipKernelTCzilahlekile ngaphambi ifayela lisebenza, ngakho-ke i-cheat ayikwazi ukuchitha ukulinganisa.- Ukuhamba kwenziwa kubhalwe ngokucacile okuwukhiqizayo. Hlela isihloko futhi uphawu luya ku-stale ngaphandle kokudlulisa kumazwana amasha.
- Uma umkhangisi ephansi uthola "ayikwazi ukuphumeza", ayikho "ilahlekile". Isimo sokuhlola ikhona emphakathini ngenxa yale sizathu.
I-Commons
Ukuqinisekiswa kubiza kakhulu; ukufundwa akuyona. I-Commons yindawo ehlukanisiwe yokulinganisa eyenza ucwaningo ngezinkinga ezivulekile ezibophelelwe yisikhathi yibhodi. Wonke umuntu angasiza, akukho muntu ophethe imiphumela, futhi wonke umsebenzi owenzayo uthola imali, kufaka phakathi othile othole lutho, ovame ukuba owaziyo.
Ubani osebenza ngayo
Halmos ikhululekile futhi incane. Uma kukhona okubi lapha, indlela elula yokukhombisa ukuthi kuyi block isiza esisebenza. Xhumanisa.