Over Halmos

Halmos is een bord voor wiskunde waar de server de wiskunde controleert. Het lijkt op elke link aggregator totdat je merkt dat sommige berichten een teken dragen dat geen enkele hoeveelheid zelfverzekerd schrijven kan produceren.

Het probleem met elk ander wiskunde forum

WiskundeOverflow, wiskunde.StackExchange, r/math, de arXiv commentaar secties. Allen hebben precies één scheidsrechter van juistheid: andere mensen, ruziën. Dat werkt opmerkelijk goed, en het is ook waarom een verkeerd bewijs geschreven vloeiend hoger rang een goed geschreven, en waarom "ik controleerde het" en "Ik geloof het" lijken identiek op de pagina.

Halmos voegt een tweede scheidsrechter toe waarmee niet kan worden geargumenteerd.

Wat de server eigenlijk doet

Plaats een omheind blok in een post of commentaar en het loopt hier, op indiening:

De output die onder een blok wordt getoond is wat het gereedschap letterlijk afgedrukt heeft. Nooit een samenvatting: samenvatting is precies waar een fabricage zou inglippen.

Hoe het te proberen, in ongeveer een minuut

1. Comment normally. De meeste berichten hebben geen wiskunde in hen helemaal en niets hier vereist. Antwoorden nest.
2. Wiskunde inline schrijven met $…$, of een displayblok met $$…$$. Het geeft als echte typent wiskunde; niets wordt uitgevoerd. Het is gewoon notatie. zie er een
3. Vraag het aan de machine. Een omheind blokje met label sage, gp, z3 of python De uitvoer is hier uitgevoerd en de output is volledig verbonden met uw post. zie er een
4. Teken iets met een plot blok (matplotlib, met plt en np klaar), of een reeks met oeis: plak de gehele getallen en het komt terug genaamd, als het bekend is.
5. Bewijs iets. A lean blok is type-gecheckt tegen Mathlib. Plakken dit in een commentaar: zie er een

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

Aanmelden is een gebruikersnaam en een wachtwoord: geen e-mail, geen bevestigingsstap. Alles wat de checkers nu doen staat op de wachtrij, en elke controleer zijn live staat is op de statuspagina: als er één neer is, wordt je verteld "niet te kunnen rennen," nooit "afgewezen."

Schrijf in je eigen tempo

Start een post en schakelen tussen schrijven en preview om uw wiskunde te zien zoals lezers zullen. Wijzigingen opslaan automatisch naar Uw ontwerpen; Spaar concept werkt ook zonder JavaScript. Concepten en previews draaien nooit code. Publiceren wanneer u klaar bent om te delen.

Gebruik rubrieken om de inhoudlijst van een artikel te bouwen. Het menu Invoegen voegt definities, theorieën, proefdrukken, voorbeelden, tabellen en links toe. Bijvoorbeeld:

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

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

Een proefdoos presenteert een argument; een geaccepteerde Lean check levert het verificatiemerk. Voeg bronnen en aangepaste LaTeX macro's onder de editor, of stel standaardwaarden in uw profiel. Kies een onderwerp en tags zodat geïnteresseerde lezers uw post kunnen vinden.

Gepubliceerde berichten hebben een postlink Bewerken. Bewaarde bewerkingen blijven privé totdat u de update publiceert. Het artikel houdt het adres van het artikel en de bestaande machinecontroles blijven gebonden aan de tekst die ze hebben gecontroleerd.

Blijf samen lezen.

Bewaar berichten in uw privé-leeslijst en volg auteurs of onderwerpen voor een persoonlijke Volgende feed. Antwoorden op uw berichten en opmerkingen verschijnen in Antwoorden op u.

Een boek of serie aanmaken om uw gepubliceerde berichten te verbinden. Voeg hoofdstukken toe, orden hun bestelling en maak de inhoud openbaar wanneer ze klaar zijn. Een privécollectie verbergt de inhoudslijst; de berichten blijven afzonderlijk gepubliceerd.

Het teken

∎ wordt een halmos, na Paul Halmos, die het einde-van-proof symbool introduceerde. Het is het enige op deze site dat autoriteit draagt, dus het is opzettelijk moeilijk om te krijgen:

• Alleen Lean kan het instellen. True is bewijs, geen bewijs.
• sorry, native_decide, een verse axiom, unsafe en debug.skipKernelTC afgewezen voor het bestand draait, dus een bedrieger kan niet eens berekenen.
• Een run wordt gepind op de exacte tekst die het geproduceerd. Bewerk de post en het teken gaat oud in plaats van over te dragen naar nieuwe woorden.
• Als een controle is beneden krijg je "kon niet uitvoeren", nooit "verworpen". Controlestatus Daarom is het openbaar.

De Commons

Verificatie is goedkoop; ontdekking niet. De Commons is een gedeelde pool van rekenwerk dat grinds op de open problemen dit bord heeft gestemd. Iedereen kan bijdragen aan het, niemand bezit het resultaat, en elke run het fondsen is openbaar, inclusief degenen die nergens, die meestal de informatieve degenen.

Wie runt het?

Halmos is onafhankelijk en klein. Als er iets mis is, kan de server het snelst bewijzen dat het een blok is. Neem contact op.