O Halmosu

Halmos je forum za matematiku gdje server provjerava matematiku. Izgleda kao bilo koji link agregator dok ne primijetite da neki postovi nose oznaku da se ne može proizvesti nikakva količina pouzdanog pisanja.

Problem sa svim drugim matematičkim forumima je

MathOverflow, math.StackExchange, r/math, arXiv komentari. Svi oni imaju tačno jednog arbitra ispravnosti: drugi ljudi, raspravljaju. To radi zapanjujuće dobro, i to je također razlog zašto pogrešan dokaz napisan tečno nadmašuje ispravan dokaz napisan loše, i zašto "Ja sam provjerio" i "Ja vjerujem" izgledaju identično na stranici.

Halmos dodaje drugog arbitra sa kojim se ne može raspravljati.

Šta server zapravo radi

Stavi ograđeni blok u bilo koji post ili komentar i on će se pokrenuti ovdje, na podnošenju:

Blok	Šta se dešava?	Može li zaraditi ∎?
`lean`	Tip provjeren u odnosu na Mathlib. Kernel prihvaća dokazni termin ili ne.	Da.
`sage`	SageMath ga pokreće; stvarni izlaz je prikvačen na post.	Ne, ne, ne.
`gp`	PARI/GP ga vodi.	Ne, ne, ne.
`z3`	Z3 traži model: najbrži način da se odbaci Nešto.	Ne, ne, ne.
`python`	Sandboxed Python, output attached.	Ne, ne, ne.

Izlaz prikazan ispod bloka je ono što je alat ispisao, doslovno. Nikad sažetak: sažetak je upravo tamo gdje bi se ušuljala fabrikacija.

Kako da pokušam, za minutu.

Komentiraj normalno. Većina postova nema matematiku u njima uopće i ništa ovdje ne zahtijeva bilo kakvu.
Napiši matematičke operacije u liniju sa $…$ , ili blok prikaza sa $$…$$. Renderira kao stvarnu matematiku; ništa se ne izvršava. To je samo notacija. Vidi jedan
Pitaj mašinu. Ograđeni blok označen sage, gp, z3 ili python is executed here and its output attached to your post, verbatim. That is evidence, not proof. Vidi jedan
Nacrtaj nešto sa plot blok (matplotlib, sa plt i np spremno), ili identificirajte sekvencu sa oeis: zalijepi cijele brojeve i vrati se sa imenom, ako je poznato.
Dokaži nešto. A-M_BAR_Švedski lean blok je tip-proverjen prema Mathlib. Zalijepite ovo u bilo koji komentar: Vidi jedan

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

Prijava je korisničko ime i lozinka: nema e-maila, nema potvrde. Sve što provjeravači rade sada je na internetu. red, a svako stanje čeka je na statusna stranicaAko je jedan pao, kažu vam "nije mogao da se pokrene", nikad "odbijen".

Pišite vlastitim tempom

Započnite post i prebacivati se između pisanja i pregleda da vidite svoju matematiku kao što će čitaoci. Promjene se automatski spremaju u Vaše skice; Spremanje skice također radi bez JavaScripta. Skice i pregledi nikad ne pokreću kod. Objavi kada si spreman da podijeliš.

Koristite naslove za izgradnju spiska sadržaja članka. Meni Umetni dodaje definicije, teoreme, dokaze, primjere, tablice i linkove. Na primjer:

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

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

Okvir za dokazivanje predstavlja argument; prihvaćena Lean provjera daje oznaku za provjeru. Dodajte izvore i prilagođene LaTeX makroe ispod editora, ili postavite uobičajene vrijednosti u Vaš profilIzaberite temu i oznake tako da zainteresirani čitaoci mogu pronaći vaš post.

Objavljeni članci imaju poveznicu Izmijeni članak. Spremljena uređivanja ostaju privatna dok ne objavite ažuriranje. Članak zadržava svoju adresu, a postojeće provjere mašine ostaju vezane za tekst koji su provjerili.

Nastavi čitati zajedno.

Spremite članke na vašu privatnu listu za čitanje i pratite autore ili teme za osobni Slijedi Odgovori na vaše postove i komentare pojavljuju se u Odgovori ti.

Napravi knjigu ili seriju za povezivanje objavljenih postova. Dodajte poglavlja, uredite njihov redoslijed i učinite sadržaj javnim kada ste spremni. Privatna kolekcija skriva svoj spisak sadržaja; njegovi postovi ostaju pojedinačno objavljeni.

Oznaka

∎ je 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:

Samo Lean može da ga postavi. True To je dokaz, a ne dokaz.
sorry, native_decide, a fresh axiom, unsafe i debug.skipKernelTC Odbijene su prije Datoteka se pokreće, tako da varanje ne može potrošiti računanje.
Run je prikvačen na tačan tekst koji ga je proizveo. Uredite post i oznaka će postati zastarjela umjesto da se prenese na nove riječi.
Ako je šah dolje, dobijete "nije mogao pokrenuti", nikad "odbijeno". Status je javno iz tog razloga.

Commons

Provjera je jeftina, otkriće nije. Commons Svatko može doprinijeti, niko ne posjeduje rezultat, i svaki pokušaj koji se financira je javni, uključujući one koji nisu nigdje došli, koji su obično informativni.

Ko ga vodi?

Halmos je nezavisan i mali. Ako nešto ovdje nije u redu, najbrži način da se dokaže je blok servera koji može pokrenuti. Dođite u kontakt..