N'ihe banyere Halmos

Halmos bụ board maka mathematics ebe sava na-enyocha mathematics. Ọ dị ka ọbụla njikọ aggregator ruo mgbe ị na-ahụ na ụfọdụ posts na-eburu akara enweghị ọnụọgụgụ nke nsụgharị n'aka na-eme.

Nchegbu na-abịa

MathOverflow, math.StackExchange, r/math, arXiv comment sections. Ha niile nwere otu arbiter nke ziri ezi: ndị ọzọ, na-asị. Ọ na-arụ ọrụ nke ọma, nakwa n'ihi ya ka ihe àmà na-ezighị ezi e dere n'ụzọ dị mfe na-eburu n'uche ihe ziri ezi e dere n'ụzọ na-ezighị ezi, nakwa n'ihi ya ka "M chegharịrị ya" na "M na-atụ anya ya" na-egosipụta na ibe ahụ.

Halmos na-egbakwunye nke abụọ arbiter nke a ga-ekwenyeghị na ya.

Ihe ọbụla saraịlụ ahụ na-eme

Tinye fenced block n'ihe ọbụla post mọọbụ nkọwa na ọ na-agba ebe a, na n'ịkepụta:

Blok	Ihe na-eme	Ọ nwere ike ịba uru ∎?
`lean`	Tíìp-nnyochaala n'ebe Mathlib nọ. Karnéèlụ̀ na-anabata ihenhọrọ ngosipụta mọọbụ ọ bụghị.	Ee
`sage`	SageMath na-agba ya; ọbụla apụtapụta bụ pined na post.	Ónyénwē
`gp`	PARI/GP na-akwọ ya.	Ónyénwē
`z3`	Z3 na-eleta maka móòdù: ụzọ nke n'ụzọ n'ụzọ Wepụ ihe ọbụla.	Ónyénwē
`python`	Sandboxed Python, ọbụna ọbụna.	Ónyénwē

Ọnụọgụgụ nke a na-egosi n'okpuru blóògù bụ ihe tùlè ahụ bipụtala, n'ụzọ nkịtị. Enweghị nchịkọta: nchịkọta bụ ebe a ga-ewepụ mmegharị ahụ.

Olee otú i nwere ike inyocha ya, n'ime nkeji ole na ole

Nkọwa dị ka ọbụla. Ọtụtụ posts nwere ọbụna na-enweghị mathematics n'ime ha na-enweghị ihe ọ bụla ebe a chọrọ ọ bụla.
Debanye masịsịịs n'ime na $…$ , mọọbụ ngosi blóògù na $$…$$. Ó na-érébàtà dịka tíípsétị̀ mátéètì ọ̀fụ̀; ọ dịghị ihe a na-eme. Ó bụ naanị nnótà. hụ otu
Kwuru igwe. Blok nke émèghị̀ n'ókè sage, gp, z3 ma ọ bụ python E mepụtara ebe a na ọbụna ihenhọrọ ya ejikọtara na post gị, n'ụzọ ziri ezi. Ọ bụ ihenhọrọ, ọ bụghị ihenhọrọ. hụ otu
Dèbàtà ihe ọbụla na plot bloku (matplotlib, na plt na np n'obere, ma ọ bụ kọwaa n'obere oeis: pịa integers na ọ na-abịa azụ aha, ma ọ bụrụ na ọ bụ a ma ama.
Ngosipụta ihe ọbụla. A lean Blok ahụ bụ ụdị-nnyocha n'ebe Mathlib nọ. Pịa nke a n'ime ihe ọbụla: hụ otu

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

Nbanye bụ aha ojieme na okwuntughe: enweghị ozi-e, enweghị nzọụkwụ nkwenye. Ihe niile ndị na-enyocha na-eme ugbua bụ na Òtù, nakwa onyenhọrọ ọbụla's live state is on the status page: ọ bụrụ na otu dị ala ị ga-ekwu "agaghị arụ ọrụ", ọ dịghị "ezere".

Bipụta n'ụdị gị

Bido ndesịta ozi ndị ahụ na gbanwee n'etiti ịgụ na nlebiritụanya ka ịhụ mathematik gị dịka ndị ọgụgụ ga-eme. Ngbanwe ndị ahụ na-echekwa n'ụzọ nkịtị na Nhazi gị; Chekwaa drọwa na-arụ ọrụ na-enweghị JavaScript. Drọwa na nlebiritụanya anaghị arụ ọrụ koodị. Bipụta mgbe ị na-emepe maka ịkekọrịta.

Jiri isiokwu iji rụpụta ndesịta ihenhọrọ nke isiokwu ahụ. Menu ahụ "Tinye" na-egbakwunye nkọwa, theorems, proofs, ihenhọrọ, táàbụ̀ na njikọ. N'omume:

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

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

N'ime igbe ahụ, gosipụtara arịrịọ; nlele Lean a na-anabata na-enyekwa akara nkwenye. Tinye isi mmalite na makoro LaTeX emeredịkachọrọ n'okpuru onyeọsụgharị, mọọbụ hazie dìfọ́ọ̀ltụ̀ na profaịlụ gị. Họrọ isiokwu na akara ndị ahụ ka ndị na-agụ ya nwee ike ịchọta ozi gị.

N'ime isiokwu ndị a pụtapụtara nwere njikọ Nhazi isiokwu. Nhazi ndị a chekwara na-adịpụghị nkeonwe ruo mgbe ị na-edepụta mmelite ahụ. Akwụkwọ ahụ na-echekwa adreesị ya, nakwa nlele igwe nọ ugbua na-adịpụghị nkeonwe na ngwe ha na-enyocha.

Kwụsị ịgụ

Chekwaa isiokwu na ndesịta ịgụta akwụkwọ nkeonwe gị na hụnụ́ ndị edemede mọọbụ isiokwu maka nkeonwe N'okpuru feed. Ndepụta nke ozi gị na nkọwa na-egosi na Ndesịta ozi ndị ahụ.

Kewapụta akwụkwọ mọọbụ usoroiheomume iji banye na isiokwu gị. Tinye isiokwu, rụnye usoroiheomume ha, na mee ka ihenhọrọ ndị ahụ bụrụ nke ọha mgbe ọ nọ n'ọrụ. Nchịkọta onwe na-ekpuchi ndesịta ihenhọrọ ya; isiokwu ya na-adị n'otu n'otu.

Ụcha

∎ a kpọrọ ya a halmos, mgbe Paul Halmos, onye na-egosi na-agwụcha-of-proof sim. Ọ bụ ihe na-abịa na ebe a na-eburu ikike, ya mere ọ bụ n'ụzọ nkịtị na-agwụ ike iji nweta:

Lean ka nwere ike ihazi ya. Sage mbipụta True bụ ihe atụ, ọ bụghị ihe atụ.
sorry, native_decide, a fresh axiom, unsafe na debug.skipKernelTC E hapụla ha tupù Faịlụ ahụ na-arụ ọrụ, yabụ na ọbụna ọbụ
A na-epin'ime n'ụdị ngwe nke na-eme ya. Dezie isiokwu ahụ na akara ahụ na-aga n'ihu n'ebe ahụ ka ọ bụrụ na ọ na-ewepụ ya n'ihe ndị ọfụụ.
Ọ bụrụ na ọ̀gụ̀ọ̀gụ̀ ahụ dị ala ị ga-enweta "Enweghị ike ijikwa", ọbụla "E nweghị ike ịgụnye". Nhazi bụ nke ọha maka ihe ahụ.

Ndị n'otu

Verifikasị bụ ọnụ; discovery bụ. Ndị n'otu bụ n'ụdị n'ụdị nke compute nke na-akpụzi n'ihe ize ndụ nke a na-emechi nke a na-ahọrọ ya. Onye ọbụla nwere ike inyere ya aka, ọ dịghị onye na-echekwa nsonaazụ, nakwa ọbụla na-agbagharị ya ego bụ nke ọha na eze, gụnyere ndị ahụ na-abịaghị ebe ọ bụla, nke bụ n'ozuzu ya ndị na-enye ozi.

Onye na-agba ya

Halmos bụ ọbụla na obere. Ọ bụrụ na ihe ọbụla dị ebe a bụ ihe na-ezighị ezi, ụzọ nke ngwa ngwa iji gosi ya bụ blóòk̀ nke sava nwere ike igwu. Kpọnye.