Halmos ∎

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-blockYini ekwenzekaIngabe ithola imali ∎?
lean Uhlobo oluhlolwe ku-Mathlib. I-kernel ivuma amagama obufakazi noma ayisebenzi. Yebo
sageI-SageMath iqhuba; okuqukethwe okusemthethweni kufakwe ku-post.Akukho
gpI-PARI/GP isebenza kuyo.Akukho
z3Z3 ibheka imodeli: indlela ekhawulezayo yoku chaza into.Akukho
pythonI-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

  1. Umbono ojwayelekile. Amanye ama-posts angeke abe nama-maths kuwo wonke umuntu futhi akukho okudingayo lapha.
  2. Bhala i-mathematics engezansi nge $…$, noma iblokhi yokukhombisa ene $$…$$. Ibonisa njengezibalo zesizinda se-typeset; akukho okuqhutshwayo. Kuyinto nje inkomba. bona eyodwa
  3. Buza imishini. Ibloki elisha eliphawulwe sage, gp, z3 noma python isebenza lapha futhi ikhishwa kwayo lixhunywe ku-post yakho, ngokucacile. Lokhu kuyiqiniso, hhayi bufakazi. bona eyodwa
  4. Dweba into ethile nge plot block (matplotlib, with plt futhi np ukulungele), noma ukhomba umkhondo nge oeis: chofoza inani eliphelele futhi lizobuyela ngegama, uma liziwa.
  5. Ubufakazi bokuthi kukhona okuthile. A-M_BAR_Isi-Italian lean i-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 True ikhombisa, hhayi ikhombisa.
  • sorry, native_decide, i-fresh axiom, unsafe futhi debug.skipKernelTC zilahlekile 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.

Xhumana nokuxhumana.

Ngena ukuze ubhale, ugcine imibono, futhi ulandele abantu abakukhuthazayo.

Dala i-akhawunti · Ukhohliwe igama lokungena?

Igama lomsebenzisi nephasiwedi yilokho okudingayo ukuqalisa.

Thumela ubufakazi

Sitshele ukuthi kwenzekani noma yini olindele. Sifunda wonke umlayezo.

Sibonga, siyithole. Uma ushiye i-imeyili sizophendula.