O Halmosu

Halmos je rada pro matematiku, kde server kontroluje matematiku. Vypadá to jako jakýkoli odkaz aggregator, dokud si všimnete, že některé příspěvky nesou značku žádné množství sebevědomého psaní může produkovat.

Problém s každým dalším matematickým fórem

MathOverflow, matematika.StackExchange, r/math, arXiv comment sekce. Všechny z nich mají přesně jeden arbitr správnosti: ostatní lidé, argumentuje. To funguje pozoruhodně dobře, a to je také důvod, proč špatný důkaz napsaný plynně nadpíše právo jeden špatně napsaný, a proč "já jsem to zkontroloval" a "Já tomu věřím" vypadají stejně na stránce.

Halmos přidává druhého arbitra, se kterým se nelze hádat.

Co server vlastně dělá?

Dejte oplocený blok na jakémkoli místě nebo komentář a běží zde, na podání:

Výstup zobrazený pod blokem je to, co nástroj vytištěn, doslovně. Nikdy shrnutí: Shrnutí je přesně tam, kde by výroba sklouzla.

Jak to zkusit, asi za minutu

1. Obvykle Comment. Většina příspěvků v nich nemá matematiku a nic tady nepotřebuje hnízdo.
2. Napsat matematiku v řádku s $…$, nebo zobrazovací blok s $$…$$. Vytváří to jako skutečné typy matematiky, nic se nestane, je to jen notace. viz jeden
3. Zeptej se toho stroje. Označený oplocený blok sage, gp, z3 nebo python is executed here and its output attached to your post, verbatim. That is evidence, not proof. viz jeden
4. Nakresli něco. s plot blok (matploglib, s plt a np připravené), nebo identifikovat posloupnost s oeis: vložte celá čísla a vrátí se pojmenovaný, pokud je známo.
5. Dokaž něco. A lean blok je typově kontrolován proti Mathlibu. Vložte to do jakéhokoliv komentáře: viz jeden

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

Zaregistrování je uživatelské jméno a heslo: žádný email, žádný kontrolní krok. Vše, co dáma dělá právě teď, je na frontaA každý šachový stát je na stavová stránka: Pokud je jeden dole, je vám řečeno "nemůžete běžet," nikdy "odmítnout."

Piš si svým vlastním tempem.

Spustit příspěvek a přepnout mezi psaním a náhledem vidět svou matematiku jako čtenáři bude. Změny uložit automaticky Vaše návrhy; Uložit draft také pracuje bez JavaScriptu. Drafty a náhledy nikdy spustit kód. Publikovat, když jste připraveni sdílet.

Použijte nadpisy pro sestavení seznamu obsahu článku. V menu Vložit přidá definice, věty, důkazy, příklady, tabulky a odkazy. Například:

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

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

Důkazní pole uvádí argument; akceptovaná kontrola Lean dodává ověřovací značku. Přidat zdroje a vlastní LaTeX makra pod editorem, nebo nastavit výchozí hodnoty v Váš profil. Vyberte téma a značky, aby zájem čtenáři mohou najít svůj příspěvek.

Publikované příspěvky mají odkaz Edit post. Uložené úpravy zůstávají soukromé, dokud nezveřejníte aktualizaci. Článek si ponechá svou adresu a stávající kontroly stroje zůstanou vázány na text, který kontrolovali.

Čti spolu.

Uložit příspěvky do svého soukromého seznamu čtení a sledovat autory nebo témata pro osobní Následující Přidat. Odpovědi na vaše příspěvky a komentáře se objeví v Odpovědi na tebe.

Vytvořit knihu nebo sérii propojit své publikované příspěvky. Přidat kapitoly, uspořádat jejich objednávku, a obsah zveřejnit, když je připraven. Soukromá sbírka skrývá svůj obsah seznam; jeho příspěvky zůstávají zveřejněny jednotlivě.

Značka

∎ se nazývá a halmos, Po Paul Halmos, který představil konec-of-proof symbol. Je to jediná věc na této stránce, která nese autoritu, takže je úmyslně těžké získat:

• Pouze Lean to může nastavit. True je důkaz, ne důkaz.
• sorry, native_decide, čerstvé axiom, unsafe a debug.skipKernelTC jsou odmítnuty předtím soubor běží, takže podvod nemůže ani utratit spočítadlo.
• Spustit je připíchnuto k přesnému textu, který jej vytvořil.Upravit příspěvek a značka se zastaralý, spíše než přecházet na nová slova.
• Když je dole dáma, dostaneš "nelze spustit"Nikdy. "odmítnuto". Stav kontroly je z tohoto důvodu veřejný.

Commons

Ověření je levné, ale objev ne. Commons je sdílený soubor výpočtů, který se zabývá otevřenými problémy, které tato rada hlasovala. Každý může přispět k tomu, nikdo vlastní výsledek, a každý způsob, jak to finanční prostředky je veřejná, včetně těch, které se nedostaly nikam, které jsou obvykle informativní ty.

Kdo to řídí?

Halmos je nezávislý a malý. Pokud je něco tady špatně, nejrychlejší způsob, jak dokázat, že je blok server může spustit. Ozvi se..