O Halmosie

Halmos jest tablicą matematyki, gdzie serwer sprawdza matematykę. Wygląda to jak każdy agregator linku, dopóki nie zauważysz, że niektóre posty nie posiadają znaku żadnej pewności pisania może wyprodukować.

Problem z każdym innym forum matematyki

MathOverflow, matematyka.StackExchange, r/math, sekcje komentarza arXiv. Wszystkie z nich mają dokładnie jeden arbiter poprawności: inni ludzie, argumentują. To działa niezwykle dobrze, a to jest również dlaczego zły dowód napisany płynnie przewyższa prawidłowy napisany, i dlaczego "Sprawdziłem to" i "Weruję", wygląda identycznie na stronie.

Halmos dodaje drugi arbiter, z którym nie można się kłócić.

Co naprawdę robi serwer

Umieścić ogrodzony blok w dowolnym poście lub komentarz i jest tutaj, na poddanie:

Blok	Co się dzieje	Czy to może zarobić ∎?
`lean`	Sprawdzono typ Mathliba. Jezgro akceptuje termin dowodu, inaczej nie.	Tak.
`sage`	SageMath to sprawdza; prawdziwy wynik jest przypięty do poczty.	Nie
`gp`	PARI/GP to sprawdza.	Nie
`z3`	Z3 szuka modelu: najszybszy sposób na niepoprawne Coś.	Nie
`python`	Piaskobox piaskofonowy, dołączony do wyjścia.	Nie

Wynik pokazany pod blokiem jest tym, co narzędzie drukowane, dosłownie. Nigdy nie podsumowuj: podsumowanie jest dokładnie miejscem, w którym wymyślenie się powinie.

Jak spróbować, za chwilę

Zazwyczaj komentarz. Większość postów nie ma matematyki w nich w ogóle i nic tutaj nie wymaga żadnego. Odpowiedzi gniazdo.
Zapisz w kolejce matematyki z $…$ , lub bloku wyświetlacza z $$…$$. To jest rzeczywiste matematyki typu; nic nie jest wykonane. Jest tylko notacja. Patrz jeden
Zapytaj maszynę. Ogrodzony blok oznaczony sage, gp, z3 lub python Tutaj wykonany jest wynik, który jest do ciebie dosłownie przyłączony. Patrz jeden
Narysuj coś z plot blok (matplotlib, z plt oraz np gotowy), lub identyfikować sekwencję z oeis: wklej liczby całkowite i wróci nazwa, jeśli jest znany.
Udowodnij coś. A lean blok jest sprawdzony typem przeciwko Mathlib. Wklej to w dowolnym komentarzu: Patrz jeden

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

Podpisanie to nazwa użytkownika i hasło: bez e-maila, bez kroku potwierdzenia. Wszystko co robią teraz szachowie jest w kolejka, a stan każdego szachera jest na strona stanu: jeśli jeden jest w dół, powiedziano "nie można uciec", nigdy "odrzucony".

Napisz w swoim tempie

Rozpocznij post i przełącza między pisaniem i podglądem, aby zobaczyć matematykę jako czytelników. Zmiany zapisz automatycznie do Twoje projekty; Zapisz projekt także działa bez JavaScript. Projekty i podglądy nigdy nie uruchamiają kodu. Opublikuj kiedy jesteś gotowy do udostępnienia.

Użyj nagłówków do zbudowania listy treści artykułu. Menu Wstaw dodaje definicje, teoremy, dowody, przykłady, tabele i linki. Na przykład:

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

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

Pole dowodowe przedstawia argument; akceptowane kontrolowanie Lean dostarcza znak weryfikacji. Dodaj źródła i niepożądane makro LaTeX pod edytorem lub ustaw domyślne profil. Wybierz temat i tagi, tak zainteresowane czytelniki mogą znaleźć swój post.

Opublikowane wpisy mają link Edytuj pocztowy. Zapisywane edycje pozostają prywatne do czasu opublikowania aktualizacji. Artykuł zachowuje swój adres, a istniejące kontrole maszynowe pozostają związane z tekstem, który sprawdzili.

Czytaj dalej.

Zapisz wpisy do listy prywatnej czytania i śledź autorów lub tematy dla osobistego Następujące feed. Odpowiedzi na Twoje posty i komentarze pojawiają się w Odpowiedzi do ciebie.

Utwórz książkę lub serię Aby połączyć opublikowane posty. Dodaj rozdziały, zorganizuj ich zamówienie i upublicznij zawartość, gdy będziesz gotowy. Własność prywatna ukrywa listę treści; jej posty pozostają publikowane indywidualnie.

Znak

∎ nazywa się halmos, Po Paul Halmos, który wprowadził symbol końcowy-of-odporny. To jedyna rzecz na tej stronie, która nosi władzę, więc jest celowo trudno dostać:

Tylko Lean może go ustawić. True to dowód, nie dowód.
sorry, native_decide, świeża axiom, unsafe oraz debug.skipKernelTC odrzuca się przed plik działa, więc oszustwo nie może nawet wydać obliczeń.
Uruchomienie jest przyklejone do dokładnego tekstu, który go wyprodukował. Edytuj post i znak jest zastarzałym zamiast przenoszenia do nowych słów.
Jeśli jest śledzony, dostaniesz "nie można uruchomić", nigdy "odrzucono". Status kontroli jest publiczny z tego powodu.

Społeczności

Weryfikacja jest tania; odkrycie nie jest. Społeczności jest wspólnym zbiorem obliczeń, które tkwi w otwartych problemach, które ta rada głosowała. Każdy może wnieść wkład w to, nikt nie posiada wyników, a każdy jego bieg jest publiczny, w tym te, które nie dostały się do niczego, które są zwykle te informatywne.

Kto to prowadzi?

Halmos jest niezależny i mały. Jeśli coś tutaj jest nie tak, najszybciej można to udowodnić, że jest blokiem, który może uruchomić serwer. Skontaktuj się.