Për Halmos

Halmos është një forum për matematikë ku serveri kontrollon matematikën. Duket si çdo agregator lidhjesh deri sa të vëreni se disa postime mbajnë një shenjë që nuk mund të prodhohet nga shkrimi i sigurt.

Problemi me çdo forum tjetër matematikor

MathOverflow, math.StackExchange, r/math, seksione komentesh arXiv. Të gjitha kanë një arbitër të saktë të saktësisë: njerëzit e tjerë, argumentojnë. Kjo punon jashtëzakonisht mirë, dhe është gjithashtu pse një provë e gabuar e shkruar rrjedhshëm e ka më të lartë renditjen se një e saktë e shkruar keq, dhe pse "e kontrollova" dhe "e besoj" duken identike në faqe.

Halmos shtoi një arbitrazh të dytë që nuk mund të diskutohet.

Çfarë bën serveri

Vendos një bllok të mbrojtur në çdo postim apo koment dhe ai do të fillojë këtu, kur të dërgohet:

Blloku	Çfarë ndodh?	A mund të fitojë ∎?
`lean`	Kontrolluar tip me Mathlib. Kernel pranon termin e provës ose jo.	Po
`sage`	SageMath e ekzekuton atë; rezultati i vërtetë është i lidhur me postën.	Jo.
`gp`	Pari/GP e drejton atë.	Jo.
`z3`	Z3 kërkon një model: rruga më e shpejtë për refuzo diçka.	Jo.
`python`	Python i sandboxuar, dalje e bashkuar.	Jo.

Rezultati i shfaqur nën një bllok është ai që shtypi instrumenti, fjalë për fjalë. Kurrë një përmbledhje: përmbledhja është pikërisht ku do të shtirej një fabrikim.

Si ta provosh, në rreth një minutë

Komente normale. Shumica e postimeve nuk kanë matematikë në to dhe asgjë këtu nuk kërkon ndonjë.
Shkrime matematike me $…$ , ose një bllok shfaqje me $$…$$. Ai paraqet si matematikë e vërtetë; asgjë nuk ekzekutohet. Është vetëm notacion. Shiko një.
Pyete makinën. Një bllok i shënuar me gardh sage, gp, z3 ose python is executed here and its output attached to your post, verbatim. That is evidence, not proof. Shiko një.
vizato diçka me plot blloku (matplotlib, me plt dhe np gati), ose identifikon një sekuencë me oeis: ngjite numrat e plotë dhe kthehet me emër, nëse është i njohur.
Vërteto diçka. A-M_BAR_Gjermanisht lean blloku është kontrolluar me Mathlib. Ngjite këtë në koment: Shiko një.

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

Regjistrimi është një emër përdoruesi dhe një fjalëkalim: pa email, pa hap konfirmimi. Gjithçka që kontrolluesit po bëjnë tani është në rreshta, dhe çdo kontrollues i gjendjes së gjallë është në status pageNëse njëri është poshtë, ju thuhet "nuk mund të ecni", kurrë "nuk u pranua".

Shkrime në ritmin tënd

Fillo një postim dhe ndërroje mes shkrimit dhe parashikimit për të parë matematikën tënde ashtu siç do të shohin lexuesit. Ndryshimet ruhen automatikisht në Skica juaj; Ruajtja e kodit punon edhe pa JavaScript. Kodet dhe pamja e parë nuk ekzekutojnë kurrë kod. Publiko kur je gati të ndash.

Përdor titujt për të ndërtuar listën e përmbajtjes së një artikulli. Menuja Fut shtoj përkufizime, teorema, prova, shembuj, tabela dhe lidhje. Për shembull:

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

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

Një kuti e provës paraqet një argument; një kontroll i pranuar Lean jep shenjën e verifikimit. Shto burimet dhe makrot e personalizuara LaTeX nën editor, ose vendos të paracaktuarat në Profili juajZgjidh një subjekt dhe etiketa që lexuesit e interesuar të gjejnë postimin tuaj.

Artikullet e botuara kanë një lidhje Ndrysho artikullin. Ndryshimet e ruajtura mbeten private deri sa të publikoni përditësimin. Artikulli mban adresën e tij dhe kontrollet ekzistuese të makinës mbeten të lidhura me tekstin që kanë kontrolluar.

Vazhdoni të lexoni së bashku.

Ruaj artikuj në listën private të leximeve dhe ndjek autorët apo temat për një përdorim personal Pas Përgjigjet ndaj postimeve dhe komenteve tuaja shfaqen në Përgjigjet.

Krijo një libër apo seri për të lidhur artikujt tuaj të publikuar. Shto kapituj, rregullo rendin e tyre dhe bëj përmbajtjen publike kur të jesh gati. Një koleksion privat fsheh listën e përmbajtjes së tij; artikujt e tij mbeten të publikuar individualisht.

Shënimi

∎ quhet halmos, pas Paul Halmos, i cili prezantoi simbolin e fundit të provave. Është e vetmja gjë në këtë faqe që mban autoritet, kështu që është me qëllim e vështirë të marrë:

Vetëm Lean mund ta vendosë atë. True Është provë, jo provë.
sorry, native_decide, një e freskët axiom, unsafe dhe debug.skipKernelTC janë refuzuar para File-i është i hapur, kështu që një mashtrues nuk mund të shpenzojë as kohën e llogaritjes.
Një rrjedhje është e fiksuar tek teksti i saktë që e ka prodhuar atë. Ndrysho artikullin dhe shenja do të jetë e vjetër në vend që të transferohet tek fjalët e reja.
Nëse një shigjetë është poshtë, ju merrni "E pamundur hapja e file", kurrë "refuzuar". Kontrolluesi i gjendjes është publik për këtë arsye.

Komuna

Verifikimi është i lirë; zbulimi nuk është. Komuna është një bazë e përbashkët e kompjuterave që punon në problemet e hapura që bordi ka votuar. çdokush mund të kontribuojë në të, askush nuk zotëron rezultatin, dhe çdo përpjekje që financon është publike, duke përfshirë ato që nuk shkojnë askund, të cilat zakonisht janë informata.

Kush e drejton?

Halmos është i pavarur dhe i vogël. Nëse diçka këtu është gabim, mënyra më e shpejtë për ta provuar është një bllok që serveri mund të ekzekutojë. Kontakto.