Om Halmos

Halmos er et bord for matematikk der tjeneren kontrollerer matematikken. Det ser ut som enhver lenkeaggregator inntil du merker at noen poster ikke har noe merke som ikke kan gi noen selvsikker skriving.

Problemet med alle andre matteforum

MathOverflow, matte. StackExchange, r/ math, arXiv kommentaravsnittene. Alle har nøyaktig én rett linje: andre mennesker, argumenterer. Det fungerer bemerkelsesverdig bra, og det er også grunnen til at feil bevis skrevet flytende overordner seg riktig, og hvorfor "jeg sjekket det" og "Jeg tror det" ser identisk ut på siden.

Halmos legger til en annen arbiter som ikke kan argumenteres med.

Hva tjeneren faktisk gjør

Sett en inngjerdet blokk i en hvilken som helst post eller kommentar og den kjører her, ved innsending:

Utdataene vist under en blokk er det verktøyet som ble skrevet ut, verbatim. Aldri et sammendrag: oppsummering er nøyaktig der et stoff ville gli seg inn.

Hvordan du prøver det, på omtrent et minutt

1. Merknad normalt. De fleste postene har ingen matte i seg i det hele tatt og ingenting her krever noen. Svar reir.
2. Skriv matte innvevd med $…$, eller en skjermblokk med $$…$$. Den gjengis som ekte typesett matte, ingenting blir utført. se en
3. Spør maskinen. En inngjerdet blokk merket sage, gp, z3 eller python blir kjørt her og utdataene er vedlagt din post, verbatim. Det er dokumentasjon, ikke bevis. se en
4. Tegn noe med a plot blokk (matplotlib, med plt og np (ferdig), eller identifisere en sekvens med oeis: lime inn heltallene og det kommer tilbake navngitt, hvis det er kjent.
5. Bevis noe. A lean blokka typesjekkes mot Mathlib. Lim inn dette i en kommentar: se en

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

Å signere er et brukernavn og et passord: ingen e- post, ingen bekreftelsessteg. Alt sjekkerne gjør akkurat nå er på kø, og hver sjekkers live tilstand er på statusside: hvis en er nede får du beskjed om at du ikke kan kjøre, aldri "avvist".

Skriv i ditt eget tempo

Start en post og bytte mellom skriving og forhåndsvisning for å se matematikken din slik leseren vil gjøre. Endringer lagres automatisk til Dine kladder; Lagre kladd virker også uten JavaScript. Kladd og forhåndsvisninger kjører aldri kode. Publiser når du er klar til å dele.

Bruk overskrifter til å bygge innholdslista i en artikkel. I menyen Sett inn legges det inn definisjoner, teoremer, prøvetrykk, eksempler, tabeller og lenker. For eksempel:

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

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

En prøveboks viser et argument. En godtatt Lean- sjekk gir verifiseringsmerket. Legg til kilder og selvvalgte LaTeX- makroer under redigeringen, eller sett standard- i din profil. Velg et emne og etiketter så interesserte lesere kan finne din post.

Publiserte poster har en Rediger etterlenke. Lagrede redigeringer forblir private inntil du publiserer oppdateringen. Artikkelen beholder adressen, og maskinsjekkene som finnes fra før er bundet til teksten de sjekker.

Fortsett lesingen

Lagre innlegg til din private leseliste og følg forfattere eller emner for en personlig Følgende canther. Svar på dine poster og kommentarer dukker opp i Svar til deg.

Lag en bok eller rekke for å koble sammen dine publiserte poster. Legg til kapitler, ordne rekkefølgen og gjør innholdet offentlig når du er klar. En privat samling skjuler innholdslista, dens poster blir publisert for seg.

Merket

∎ kalles a halmos, etter Paul Halmos, som introduserte symbolet for « slutten på » - tegnet. Det er det eneste på dette nettstedet som bærer autoritet, så det er bevisst vanskelig å få:

• Bare Lean kan stille det inn. Sage- utskrift True er bevis, ikke et bevis.
• sorry, native_decide, frisk axiom, unsafe og debug.skipKernelTC avvises før fila kjører, så et fusk kan ikke engang bruke regnestykkene.
• En kjøring er festet til den eksakte teksten som ga den. Rediger posten og merket blir stående i stedet for å overføre til nye ord.
• Hvis en brikke er nede får du "kunne ikke kjøre", aldri "avvist". Sjakkstatus er offentlig av den grunn.

Felleskap

Verifiseringen er billig, det er ikke mulig å finne den. Felleskap Det er en felles samling av beregninger som maler på de åpne problemene som dette brettet har brutt seg til.

Hvem kjører den

Halmos er uavhengig og liten. Hvis noe er galt, så er det den raskeste måten å bevise at det er en blokk som tjeneren kan kjøre. Kontakt.