Om Halmos

Halmos är ett forum för matematik där servern kontrollerar matematiken. Det ser ut som en länkaggregator tills du märker att vissa inlägg bär ett märke ingen mängd självsäker skrift kan producera.

Problemet med alla andra matteforum

MathOverflow, math.StackExchange, r/math, arXiv kommentarsavsnitt.Alla av dem har exakt en skiljedomare av korrekthet: andra människor, argumentera. Det fungerar anmärkningsvärt bra, och det är också därför ett felaktigt bevis som skrivit flytande överträffar en rätt skriven dåligt, och varför "Jag kontrollerade det" och "Jag tror det" ser identiskt på sidan.

Halmos lägger till en andra skiljedomare som inte kan argumenteras med.

Vad servern faktiskt gör

Sätt en inhägnad block i någon post eller kommentar och det körs här, vid inlämning:

Utmatningen som visas under ett block är vad verktyget tryckt, ordagrant. Aldrig en sammanfattning: sammanfattning är exakt där en tillverkning skulle glida in.

Hur man försöker, om en minut

1. Comment normally. De flesta inlägg har inga matematiker alls och ingenting här kräver några. Svar bo.
2. Skriv matematik inline där $…$, eller ett displayblock med $$…$$. Det återges som verkliga typsnittsmatte, ingenting utförs. Det är bara notation. se en
3. Fråga maskinen. Ett inhägnat block märkt sage, gp, z3 eller python Den utförs här och dess utdata är bifogade till din post, ordagrant. se en
4. Rita något med en plot block (matplotlib, med plt och np eller identifiera en sekvens med oeis: klistra in heltalen och det kommer tillbaka namngivet, om det är känt.
5. Bevisa nåt. A lean blocket typkontroll mot Mathlib. Klistra in det här i någon kommentar: se en

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

Att registrera sig är ett användarnamn och ett lösenord: inget e-postmeddelande, ingen bekräftelse steg. Allt som kontrollanterna gör just nu är på den kö, och varje kontroll' s levande tillstånd är på status sida: om man är nere får man höra "inte kunde springa", aldrig "avvisas".

Skriv i din egen takt

Starta ett inlägg och växla mellan skrivande och förhandsvisning för att se din matematik som läsare kommer. Ändringar spara automatiskt till Dina utkast; Spara utkast fungerar också utan JavaScript. Utkast och förhandsvisningar kör aldrig kod. Publicera när du är redo att dela.

Använd rubriker för att bygga en artikels innehållslista. Menyn Infoga lägger till definitioner, teorem, bevis, exempel, tabeller och länkar. Till exempel:

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

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

En bevisruta innehåller ett argument; en accepterad Lean-kontroll ger verifieringsmärket. Lägg till källor och anpassade LaTeX- makron under editorn, eller ställ in standardvärden i din profilVälj ett ämne och taggar så att intresserade läsare kan hitta ditt inlägg.

Publicerade inlägg har en länk till Redigera inlägg. Sparade redigeringar förblir privata tills du publicerar uppdateringen. Artikeln behåller sin adress, och befintliga maskinkontroller förblir knutna till texten de kontrollerade.

Fortsätt läsa tillsammans

Spara inlägg till din privata läslista och följ författare eller ämnen för en personlig Följande svar på dina inlägg och kommentarer visas i Svar till dig.

Skapa en bok eller serie för att ansluta dina publicerade inlägg. Lägg till kapitel, ordna deras beställning och gör innehållet offentligt när det är klart. En privat samling döljer innehållslistan; dess inlägg publiceras fortfarande individuellt.

Märket

∎ kallas för a halmos, efter Paul Halmos, som introducerade end-of-proof symbolen. Det är det enda på denna webbplats som bär auktoritet, så det är avsiktligt svårt att få:

• Bara Lean kan ställa in det. Sage utskrift True är bevis, inte bevis.
• sorry, native_decide, en färsk axiom, unsafe och debug.skipKernelTC avvisas före filen körs, så en fuskare kan inte ens spendera beräkna.
• En körning är fastsatt till den exakta texten som skapade den. Redigera inlägget och märket går gammalt snarare än att överföra till nya ord.
• Om en kontroll är nere får du "kunde inte köra", aldrig "avvisad". Kontrollstatus är offentligt av den anledningen.

Vanliga

Verifiering är billigt, upptäckt är inte. Vanliga är en delad pool av beräkningar som maler på de öppna problem som styrelsen har röstat upp. Vem som helst kan bidra till det, ingen äger resultatet, och varje körning det medel är offentlig, inklusive de som inte fick någonstans, som vanligtvis är de informativa.

Vem styr det?

Halmos är oberoende och liten. Om något här är fel, det snabbaste sättet att bevisa att det är ett block servern kan köra. Kontakta.