Halmoksesta

Halmos on matematiikan lautakunta, jossa serveri tarkistaa matematiikassa. Näyttää ihan joltakin linkin kokoajan kannalta, kunnes huomaa, että joissakin kirjoituksissa ei ole merkkiäkään varmasta kirjoittamisesta.

Ongelmana joka toisella matematiikan foorumilla

Mathoverflow, matematiikassa.StackExchange, r/math, arXiv-kommenttiosiot. Kaikilla on täsmälleen yksi korrektiuden peruste: muut ihmiset, jotka riitelevät. Se toimii hämmästyttävän hyvin, ja siksi myös väärä todiste on sujuvasti kirjoitettua huonompi ja miksi "tarkistin sen" ja "uskon sen" näyttävät samalta sivulla.

Halmos lisää toisen sovittelijan, jota ei voida kiistää.

Mitä palvelimen toiminta todellisuudessa tekee

Laita aidattu lohko mihin tahansa viestiin tai kommenttiin, ja se kulkee tässä, kun se on toimitettu:

Lohkare	Mitä tapahtuu?	Voiko se ansaita ∎?
`lean`	Kynsi on tarkastettu Mathlibiä vastaan. Ytimen mukaan todistetermi on joko hyväksyttävä tai se ei.	Kyllä
`sage`	SageMath pyörittää sitä, todellinen ulostulo on kiinni pylväässä.	Ei ole tarpeen
`gp`	PARI/GP pyörittää sitä.	Ei ole tarpeen
`z3`	Z3 etsii mallia: nopein tie kumoa Jotain.	Ei ole tarpeen
`python`	Hiekkaboksoitu Python, ulostulo liitetty.	Ei ole tarpeen

Korttelin alla näkyy työkalun paino, sanatarkasti. Ei koskaan yhteenvetoa: yhteenveto on juuri siinä, missä sekoilu sujahtaa sisään.

Miten sitä kokeillaan, noin minuutin kuluttua

Kommentoi normaalisti. Useimmissa kirjoituksissa ei ole lainkaan matematiikkaa, eikä mikään täällä vaadi mitään.
Kirjoita matematiikkaa riviin yy) $…$ , tai näyttöpalkki, jolla $$…$$. Se tekee todellisesta ladosta matematiikan; mitään ei tehdä. katso yksi
Kysy koneelta. Aidattu lohko merkitty sage, gp, z3 tai python is executed here and its output attached to your post, verbatim. That is evidence, not proof. katso yksi
Piirrä jotain jossa plot lohko (matplotlib, plt sekä np valmis) tai tunnistaa sekvenssin, jossa oeis: liitä kokonaislukuja ja se tulee takaisin nimettynä, jos se on tiedossa.
Todista jotain. A lean Block on koneella tarkastettu Mathlibiä vastaan. Liitä tämä kommenttiin: katso yksi

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

Ilmoittautuminen on käyttäjätunnus ja salasana: ei sähköpostia, ei vahvistusvaihetta. Kaikki, mitä tammet tekevät nyt, on päällä jono, ja jokaisen tarkastajan live tila on TilasivuJos yksi on kaatunut, sinulle sanotaan, että "ei voi juosta", ei koskaan "hylätä".

Kirjoita omalla tahdillasi

Aloita viesti ja siirry kirjoittamisen ja esikatselun välillä nähdäksesi matematiikkasi lukijoina. Muutokset tallentuvat automaattisesti Piirroksesi; Tallenna luonnokset toimii myös ilman JavaScriptia. Piirrokset ja esikatselut eivät koskaan käytä koodia. Julkaise, kun olet valmis jakamaan.

Lisää-valikkoon lisätään määritelmät, teoreemojen, vedosten, esimerkkien, taulukoiden ja linkkien nimet.

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

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

Todistelaatikko esittää argumentin; hyväksytty Lean-tarkistus antaa varmistusmerkin. Lisää lähteet ja muokkaimen alle muokkaimen alle muokkain LaTeX-makrot tai aseta oletukset profiilisi. Valitse aihe ja tunnisteet, jotta kiinnostuneet lukijat löytävät viestisi.

Julkaistuissa teksteissä on Edit-viestilinkki. Tallennetut muokkaukset pysyvät yksityisinä päivityksen julkaisemiseen asti. Artikkeli pitää osoitteensa ja nykyiset konetarkistukset pysyvät sidottuina tarkastamaansa tekstiin.

Jatka lukemista yhdessä

Tallenna viestit yksityiselle lukulistallesi ja seuraa kirjoittajia tai aiheita henkilökohtaiseen Seuraava rehu. Vastaukset viestiisi ja kommentteja näkyvät Vastaukset.

Luo kirja tai sarja Lisää lukuja, järjestä niiden tilaus ja julkista sisältö, kun se on valmis. Yksityiskokoelma kätkee sisältöluettelonsa, ja sen viestit julkaistaan edelleen erikseen.

Merkintä

∎ on nimeltään halmos, Paul Halmos, joka esitteli viimeisen symbolin. Se on ainoa asia tällä sivustolla, joka kantaa valtaa, joten sitä on tarkoituksella vaikea saada:

Vain Lean voi asettaa sen. True Se on todiste, ei todiste.
sorry, native_decide, tuore axiom, unsafe sekä debug.skipKernelTC hylätään ennen tiedosto kulkee, joten huijari ei pysty edes käyttämään laskelmia.
Tarkalleen tuotettuun tekstiin on kiinnitetty juoksu. Muokkaa viestiä ja merkki menee tunkkaiseksi sen sijaan, että se siirtyisi uusiin sanoihin.
Jos tammenpyyhin on alhaalla, saat "ei voinut juosta"Ei koskaan "Hylättiin". Tarkistajan tila on julkinen siitä syystä.

Alahuone

Varmennus on halpaa, löytö ei. Alahuone Se on yhteinen laskenta-aineisto, joka jauhaa avoimia ongelmia, joista hallitus on äänestänyt. Kuka tahansa voi vaikuttaa siihen, kukaan ei omista tulosta, ja jokainen sen rahoittama yritys on julkinen, mukaan lukien ne, jotka eivät ole päässeet mihinkään, jotka ovat yleensä informatiivisia.

Kuka sitä pyörittää

Halmos on riippumaton ja pieni. Jos jokin tässä on pielessä, nopein tapa todistaa, että se on lohko, jonka palvelimen voi ajaa. Ota yhteyttä.