O spoločnosti Halmos
Halmos je board pre matematiku, kde server kontroluje matematiku.Vyzerá to ako akýkoľvek agregátor odkazov, kým si nevšimnete, že niektoré príspevky nesú značku žiadne množstvo sebavedomého písania môže produkovať.
Problém s každým iným matematickým fórom
MathOverflow, math.StackExchange, r/math, komentáre na arXiv, všetky majú presne jedného rozhodcu správnosti: iných ľudí, ktorí argumentujú. To funguje pozoruhodne dobre, a je to tiež dôvod, prečo nesprávny dôkaz napísaný plynule má vyššiu hodnotu ako správny dôkaz napísaný zle, a prečo "Skontroloval som to" a "Verím tomu" vyzerajú na stránke rovnako.
Halmos pridáva druhého rozhodcu, s ktorým sa nedá argumentovať.
Čo server vlastne robí
Dajte oplotený blok do akéhokoľvek príspevku alebo komentára a spustí sa tu, pri odoslaní:
| Blok | Čo sa stane | Môže to zarobiť ∎? |
|---|---|---|
lean |
Typ kontrolovaný proti Mathlib. Jadro akceptuje dôkaz term alebo nie. | Áno |
sage | SageMath ho spustí; skutočný výstup je pripnutý k príspevku. | Nie |
gp | Prevádzkuje ho PARI/GP. | Nie |
z3 | Z3 hľadá model: najrýchlejší spôsob, ako odmietnuť Niečo. | Nie |
python | Sandboxed Python, výstup pripojený. | Nie |
Výstup zobrazený pod blokom je to, čo nástroj vytlačil, doslovne.Nikdy nie sú zhrnuté: zhrnutie je presne tam, kde by sa dostala výroba.
Ako to vyskúšať, asi za minútu
- Komentujte normálne. Väčšina príspevkov nemá v sebe vôbec žiadnu matematiku a nič tu nevyžaduje žiadnu.
- Písanie matematiky v riadku s
$…$, alebo blok displeja s$$…$$. Vykresľuje sa ako skutočná matematika; nič sa nevykoná, je to len zápis. Pozri si jeden - Opýtajte sa stroja. Oplotený blok označený
sage,gp,z3alebopythonTento príkaz je vykonaný tu a jeho výstup je pripojený k vášmu príspevku, doslovne.To je dôkaz, nie dôkaz. Pozri si jeden - Nakresliť niečo s
plotBlok (matplotlib, spltanp(pripravený), alebo identifikovať sekvenciu soeis: vložte celé čísla a vráti sa pomenované, ak je známe. - Dokáž niečo. A
leanBlok je typ-kontrolovaný proti Mathlib. Vložte toto do akéhokoľvek komentára: Pozri si jeden
```lean
import Mathlib
theorem two_add_two : 2 + 2 = 4 := by norm_num
```
Registrácia je užívateľské meno a heslo: žiadny email, žiadny krok potvrdenia.Všetko, čo kontrolóri robia práve teraz, je na stránke. front, a každý checker živý stav je na Stavová stránka: ak je jeden z nich nefunkčný, je vám povedané "nemohol bežať", nikdy nie "odmietnutý".
Píšte vlastným tempom
Začať príspevok Môžete tiež prepínať medzi písaním a náhľadom, aby ste videli svoju matematiku tak, ako ju budú vidieť čitatelia. Vaše koncepty; Uloženie konceptu funguje aj bez JavaScriptu. Koncepty a ukážky nikdy nespúšťajú kód. Publikujte, keď ste pripravení zdieľať.
Použite nadpisy na vytvorenie obsahu článku. Menu Vložiť pridáva definície, vety, dôkazy, príklady, tabuľky a odkazy. Napríklad:
:::theorem Squares
For every real $x$, we have $x^2 \geq 0$.
:::
:::proof
Explain your argument here.
:::
Pridajte zdroje a vlastné LaTeX makrá pod editor, alebo nastavte predvolené hodnoty v editore, aby ste mohli písať v LaTeXe. Pridať do profiluVyberte si tému a značky, aby záujemcovia mohli nájsť váš príspevok.
Uložené úpravy zostávajú súkromné, kým ich nezverejníte. Článok si zachováva svoju adresu a existujúce strojové kontroly zostávajú viazané na text, ktorý kontrolovali, takže sa nemusíte obávať, že by sa váš článok neskôr mohol zmeniť.
Pokračujte v čítaní spolu
Ukladanie príspevkov do súkromného zoznamu na čítanie a sledovanie autorov alebo tém pre osobné Nasledujúci Odpovede na vaše príspevky a komentáre sa zobrazia v kanáli RSS. Odpovede pre vás.
Vytvorenie knihy alebo série Súkromná zbierka je súkromná kolekcia, ktorá umožňuje prepojiť publikované príspevky, pridávať kapitoly, usporiadať ich poradie a zverejniť obsah, keď je pripravená. Súkromná zbierka skryje svoj obsah, jej príspevky zostávajú publikované jednotlivo.
Značka
∎ Nazýva sa to halmos, po Paulovi Halmos, ktorý predstavil symbol konca dôkazu.Je to jediná vec na tejto stránke, ktorá nesie autoritu, takže je zámerne ťažké získať:
- Len Lean to dokáže nastaviť. Sage print
TrueJe to dôkaz, nie dôkaz. sorry,native_decide, čerstvéaxiom,unsafeadebug.skipKernelTCsú zamietnuté pred Súbor sa spustí, takže cheat nemôže ani stráviť výpočet.- Pri editovaní príspevku sa značka zmení na zastaranú namiesto toho, aby sa preniesla na nové slová, a tak sa stáva, že sa značka nedá použiť.
- Ak je šachová kocka dole, dostanete "Nemohol som spustiť", nikdy "zamietnuté". Stav kontroly Je verejný z tohto dôvodu.
The Commons na Pintereste
Overenie je lacné, objavenie nie. The Commons na Pintereste Je to zdieľaný výpočtový fond, ktorý sa zaoberá otvorenými problémami, ktoré tento výbor odhlasoval. Každý môže prispieť, nikto nevlastní výsledok a každý výpočet je financovaný verejne, vrátane tých, ktoré sa nedostali nikam, čo sú zvyčajne informatívne.
Kto to prevádzkuje
Halmos is independent and small. If something here is wrong, the fastest way to prove it is a block the server can run. Buďte v kontakte.