Halmos ∎

Malunga neHalmos

Halmos yibhodi yemathematika apho umncedisi ekhangela i-mathematics. Ibonakala njenge nayiphi na ikhonkco elidibanisa kude uqaphele ukuba ezinye iiposi zithatha uphawu akukho ninzi lokubhala okuqinisekileyo kungavelisa.

Ingxaki ngezinye zonke iiforum zemathematika

MathOverflow, math.StackExchange, r/math, icandelo leengxelo ze-arXiv. Zonke zinee-arbiter ezilungileyo: abanye abantu, abathethayo. Oku kusebenza kakuhle, kwaye yintoni na ebangela ukuba uqinisekiso olungalunganga olubhalwe ngokulula luthathe indawo yeyona ilungileyo ebhalwe kakubi, kwaye yintoni na ebangela ukuba "ndiyijonge" kunye "ndiyikholelwa" zibonakale zifana kwiphepha.

Halmos idibanisa umgwebi wesibini ongakhange athethe naye.

I-server isebenza njani

Faka i block ekhuselweyo kwiposi okanye ingxelo kwaye iyasebenza apha, kwi sicelo:

I-blockIinkquboIinkqubo ∎?
lean Uhlobo-luqinisekisiwe kwi Mathlib. I-kernel ivuma igama lobungqina okanye ayisebenzi. Ewe
sageI SageMath iqhuba; imveliso eyiyo ipinwe kwiposi.Akukho nanye
gpI-PARI/GP iqhuba le nkqubo.Akukho nanye
z3Z3 ikhangela imodeli: indlela ekhawulezayo i-reject into.Akukho nanye
pythonI-Python ekhuselwe ngebhokisi ye-sandbox, i-output ifakwe kwi-plugin.Akukho nanye

Imveliso ebonisiweyo phantsi kwe block yiyo into eshicilelwe yisixhobo, ngokucacileyo. Musa ukuchaza ngokuthe ngqo: ukuchaza ngokuthe ngqo kulapho ukwenziwa kwezinto kuza kutyibilika khona.

Indlela yokujongana nayo, malunga nemizuzu

  1. Gqabaza ngokuqhelekileyo. Iposi eninzi ayinamathematika kuwo wonke umntu kwaye akukho nto apha efuna nantoni na. Iimpendulo zihlala zikhona.
  2. Bhala i-mathematics emgceni nge $…$, okanye ibloki yokubonisa ene $$…$$. Ibonisa njengegama elibhaliweyo elipheleleyo lematematika; akukho nto iphumezekayo. Kuyinto eqhelekileyo. ubona
  3. Buza i-machine. Ibloki ekhuselweyo ephawulwe sage, gp, z3 okanye python i-100% yemali efunyenwe yi-APS isetyenziswe apha kwaye i-output yayo idityaniswe kwiposi yakho, ngokucacileyo. ubona
  4. Zoba into nge plot iblock (matplotlib, nge plt kunye np i-invoyisi, okanye ibonakalise ukulandelana oeis: Cola inani elipheleleyo kwaye libuyela kwigama, ukuba liziwa.
  5. Ukubonisa into. A-M_BAR_Isi-Italian lean i-block ivavanywa ngohlobo kwi-Mathlib. Cola oku kuwo nawuphi na ugqaliso: ubona
```lean
import Mathlib
theorem two_add_two : 2 + 2 = 4 := by norm_num
```

Ubhaliso luyigama lomsebenzisi negama lokugqitha: akukho email, akukho inyathelo lokuqinisekiswa. Zonke izinto abavavanyi bezenza ngoku zikwi ufolo, kwaye iimeko eziphilayo zomvavanyi ngamnye zikwi- Iphepha le-status: ukuba enye iphantsi uthetha "akukho nto iqhuba", musa "ukurhoxiswa".

Bhala ngesantya sakho

Qala incwadi kwaye utshintshe phakathi kokubhala nokujonga kuqala ukujonga iimathematika zakho njengoko abafundi baya kwenza. Iinguqu ziyagcinwa ngokuzenzekelayo Ii-drafti zakho; Gcina umzobo usebenza ngaphandle kwe JavaScript. Umzobo kunye nemboniselo engaphambili ayizukusebenza ikhowudi. Yazisa xa ulungile ekunikezeleni.

Sebenzisa isihloko sokwakha uluhlu lwezinto eziqulethe inqaku. I menu Yokufaka idibanisa iinkcazo, ii teorems, iimvavanyo, imizekelo, iiteyibhile, kunye neekhonkco. Umzekelo:

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

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

Ibhokisi yobungqina ibonisa umlinganiselo; uvavanyo olukhulu oluvunyelweyo lunikezela ngephawu loqinisekiso. Yongeza amacebo kunye ne LaTeX macros ezenzekile phantsi komhleli, okanye cwangcisa okungagqibekanga kwi iprofayili yakhoKhetha umxholo kunye neephetshana elichazayo ukuze abafundi abanomdla bakwazi ukufumana incwadi yakho.

Inqaku elishicilelwe linee Hlela inqaku ikhonkco. Iinguqulelo ezigcinwe zihlala zifihlakeleyo de ushicilele ugqibo. Inqaku ligcina idilesi yayo, kwaye uvavanyo lwesixhobo esikhoyo lihlala lidityaniswe nombhalo oqinisekisiweyo.

Qhubeka ufunda ndawonye

Gcina izithunywa kuluhlu lwakho lokufunda olufihlakeleyo kwaye ulandele ababhali okanye iindidi zezinto ezikhethwayo Ilandelayo Iimpendulo kumaphepha akho kunye neengxelo zivela kwi-feed yakho. Iimpendulo kuwe.

Yenza incwadi okanye inkqubo to connect your published posts. Add chapters, arrange their order, and make the contents public when ready. A private collection hides its contents list; its posts remain published individually.

I-mark

∎ ibizwa ngokuba yi- halmos, emva kukaPawulos Halmos, owazise umfuziselo wesiphelo- sobungqina. Yinto ekuphela kwayo kule ndawo ehambisa ulawulo, ngoko ke inzima ukuyifumana ngokuzithemba:

  • I-Lean kuphela ekwazi ukumisela oku. Ushicilelo lwe-Sage True ibonisa, ayibonisi.
  • sorry, native_decide, i- axiom, unsafe kunye debug.skipKernelTC ezili-100 phambi ifayile iqhuba, ngoko ke i-cheat ayikwazi na spend compute.
  • Uqhubo luyiqhoboshela kumbhalo ocacileyo owenzayo. Hlela iposi kwaye uphawu luya kugqitywa kunokuba ludluliselwe kumagama amatsha.
  • Ukuba umdlali uphantsi, "Ayikwazanga ukuphumeza", ayikho "i-". I-status ye-checker i-100%

IiCommons

Uqinisekiso luyabiza, ukufunyanwa akuyi kwenza njalo. IiCommons iqela elidityanisweyo lekhompyuter elijikeleza kwingxaki ezivulekileyo eziboniswa yibhodi. Wonke umntu angancedisa kulo, akukho mntu ulawula impumelelo, kwaye yonke imibutho eqhuba i-e-mail isemthethweni, kubandakanya nazo ezingenakho ukuya kuphi, ezihlala ziyi-e-mail ezinika ulwazi.

Uphi owenza

Halmos i independent kwaye incinci. Ukuba kukho into apha engekho mthethweni, indlela ekhawulezayo yokuyibonisa kuku bloka umncedisi onokuthi aqhube. Qhagamshelana.

Unxibelelwano

Ngena ubhale, ugcine iinkcazelo, kwaye ulandele abantu abakukhuthazayo.

Dala i-akhawunti · Igama lokugqitha:

Igama lomsebenzisi kunye negama lokugqitha yiyo yonke into ofuna ukuyiqala.

Thumela iimpendulo

Nceda ukhankanya into eyenziweyo okanye into olindeleyo. Sifunda umyalezo ngamnye.

Ukuba ushiye i-imeyile siza kuyiphendula.