Omtrent Halmos
Halmos is a board for mathematics where the server checks the mathematics. It looks like any link aggregator until you notice that some posts carry a mark no amount of confident writing can produce.
Die probleem met elke ander wiskunde forum
Math overflow, wiskunde. Strigixchange, r/math, die arXiv kommentaar dele. Hulle het almal presies een arbiter van korrektheid: ander mense, stry. Dit werk merkwaardig goed, en dit is ook waarom 'n verkeerde bewys wat vlot geskryf is 'n regte een geskryf sleg, en waarom "Ek dit nagegaan" en "Ek glo dit" kyk op die bladsy.
Halmos adds a second arbiter that cannot be argued with.
Wat die bediener werklik doen
Plaas 'n versterkte blok in enige pos of kommentaar en dit hardloop hier, op onderdanigheid:
| Blok | Wat gebeur | Kan hy verdien ∎? |
|---|---|---|
lean |
Type-toets teen Mathlib. Die kernel aanvaar die bewys term of dit doen nie. | Ja |
sage | Die velmath hardloop dit; die ware afvoer word aan die pos vasgepen. | Nee |
gp | PARAD/GP loop dit. | Nee |
z3 | Z3 soek vir 'n model: die vinnigste manier na weerlê iets. | Nee |
python | Sandboksed Python, uitset vas. | Nee |
Die afvoer wat onder'n blok vertoon word, is wat die instrument gedruk, woord vir woord.'n Opsomming:'n opsomming is presies waar'n versinsel sal verdwyn.
Hoe om dit te probeer, in omtrent 'n minuut
- Kommentaar gewoonlik. Die meeste poste het geen wiskunde daarin nie en niks hier vereis enige nie.
- Skryf wiskunde inlyn met
$…$, of'n vertoonblok met$$…$$. Dit gee as werklike druk wiskundee weer; niks word uitgevoer nie. sien een - Vra die masjien. ' n Gekampde blok word gemerk
sage,gp,z3ofpythonhier tereggestel word en die afvoer wat aan jou pos vasgemaak is, werkwoordaim. sien een - Teken iets met â n
plotblok (matplotlib, metpltennpgereed), of identifiseer 'n volgorde metoeis: plak die heelgetalle en dit kom terug na die naam, as dit bekend is. - Wys iets. A
leanblok is tipe-toets teen Mathlib. Plak hierdie in enige kommentaar: sien een
```lean
import Mathlib
theorem two_add_two : 2 + 2 = 4 := by norm_num
```Teken begin is 'n gebruikernaam en' n wagwoord: nee e- pos, nee bevestiging stap. Alles wat die kontrolers doen doen nou is op die tou, en elke tjeker se lewenstoestand is op die statusblad: As iemand onder is, kan jy "nie hardloop nie", nooit "uitgespuit" nie.
Skryf teen jou eie pas
Begin 'n pos en wissel tussen skryf en voorskou om jou wiskunde as lesers te sien. Veranderinge stoor outomaties na Jou invoerings; Stoor proses ook werk sonder Javaskrip. Rofwerk en voorskoue loop nooit kode nie. Voorskou wanneer jy gereed is om te deel.
Gebruik opskrifte om 'n artikel se inhoudlys te bou. Die invoeg kieslys voeg definisies, teoreems, bewyss, voorbeelde, tabelle en skakels by. Byvoorbeeld:
:::theorem Squares
For every real $x$, we have $x^2 \geq 0$.
:::
:::proof
Explain your argument here.
:::'n Toets boks bied 'n argument;' n aanvaarde Lean tjek verskaf die bevestiging merk. Voeg by bronne en pasmaak LaTeX makros onder die redigeerder, of stel versteke in profiel. Kies'n onderwerp en merkers wat so belangstel, lesers kan jou pos kry.
Uitgegeede pale het 'n Redigeer post skakel. Gestoor redigeer bly privaat totdat jy die dateer op. Die artikel hou sy adres, en bestaande masjien tjeks bly vasgebind aan die teks wat hulle nagegaan het.
Hou aan lees saam
Stoor poste na jou eie lees lys en volg outeurs of onderwerpe vir 'n persoonlike Volgende wei. Antwoorde op jou poste en kommentare verskyn in Antwoorde op jou.
Skep 'n boek of reeks om u gepubliseerde deurposte te verbind. Voeg hoofstukke by, reël hulle volgorde en maak die inhoud oop wanneer dit gereed is. 'n private versameling verberg sy inhoudlys; sy deurposte bly individueel gepubliseer.
Die merk
∎ word a genoem halmos, after Paul Halmos, who introduced the end-of-proof symbol. It is the only thing on this site that carries authority, so it is deliberately hard to get:
- Net Lean kan dit stel, en die druk van die aar
Trueis bewys, nie'n bewys nie. sorry,native_decide, 'n nuweaxiom,unsafeendebug.skipKernelTCverwerp word voor Die lêer loop, dus kan 'n kul nie eers bereken nie.- 'n lopie word gepenneer aan die presiese teks wat dit vervaardig. Redigeer die pos en die merk gaan our as oorplas na nuwe woorde.
- As'n toetser af is, kry jy "kon nie hardloop nie", nooit "Verwerp". Merkerstatus is om daardie rede bekend.
Die algemenes
Verifikasie is goedkoop; ontdekking is nie. Die algemenes is'n gemeenskaplike poel van bereken wat op die oop probleme maal wat hierdie raad verkies het.'n Mens kan dit ook doen, niemand besit nie en elke fooi geld is publiek, insluitende dié wat nêrens gekom het nie, wat gewoonlik die leersames is.
Wie hardloop
Halmos is onafhanklik en klein. As iets hier is verkeerde, die vinnigste manier om te bewys dit is 'n blok die bediener kan hardloop. Raak in aanraking.