Apie Halmos

Halmos yra matematikos lenta, kur serveris tikrina matematiką. Atrodo, kad bet nuoroda Agregator kol pastebite, kad kai kurie pranešimai turi ženklą jokios patikimos rašymo gali gaminti.

Problema su visais kitais matematikos forumas

MathOverflow, matematika.StackExchange, R / matematika, arXiv komentaras skyrius. Visi jie turi tiksliai vieną teisingumo arbiterį: kiti žmonės, argumentuoja. Tai veikia nepaprastai gerai, ir tai taip pat kodėl neteisingas įrodymas parašyta laisvai išskleidžia dešinį vieną parašyta blogai, ir kodėl "Aš ją patikrinau" ir "Aš manau, kad jis" atrodo identiškas puslapyje.

Halmos prideda antrą arbiter, su kuriuo negalima ginčytis.

Ką iš tikrųjų veikia serveris

Įdėkite tvoros bloką bet paštu ar komentaras ir ji veikia čia, pateikimo:

Po bloku rodomas išvestis yra tai, ką išspausdintas įrankis, stenograma. Niekada santrauka: apibendrinantis yra tiksliai ten, kur gamyba būtų paslysti.

Kaip pabandyti, maždaug minutėlę

1. Komentuokite normaliai. Dauguma pranešimų neturi matematikos jų visi ir nieko čia nereikia. Atsakymai lizdas.
2. Įrašyti matematiką į eilę kai: $…$arba ekrano blokas, kuriame $$…$$. Jis atvaizduoja kaip realius rašominius matematikus; nieko nėra įvykdyta. Tai tik įrašas. žr.
3. Paklausk mašinos. Užtvindytas blokas su įstrižainiais sage, gp, z3 arba python yra įvykdytas čia ir jos rezultatas pridedamas prie jūsų posto, stenograma. Tai yra įrodymas, ne įrodymas. žr.
4. Piešti ką nors su plot blokas (matplotlib, su plt ir np yra) arba nustatyti seką, kai oeis: įklijuoti sveikuosius skaičius ir jis grįžta pavadintas, jei jis yra žinomas.
5. Įrodyk ką nors. A lean blokas yra tipo patikrintas prieš Mathlib. Įdėti tai į bet komentarą: žr.

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

Pasirašymas yra naudotojo vardas ir slaptažodis: nėra el. pašto, nėra patvirtinimo žingsnis. Viskas, ką tik tikrinantieji daro dabar, yra ant eilėir kiekvieno tikrinančio asmens gyva būsena yra ant būsenos puslapis: jei vienas yra žemyn, jums pasakyta "negali paleisti", niekada "atmestas".

Rašyk savo pačių tempu

Pradėti pranešimą ir pereiti tarp rašymo ir peržiūros, kad pamatytų savo matematiką, kaip skaitytojai bus. Pakeitimai įrašyti automatiškai Jūsų projektai; Išsaugoti projektą taip pat veikia be JavaScript. Projektai ir peržiūros niekada paleisti kodą. Leidinys, kai esate pasirengę pasidalinti.

Naudoti antraštes straipsnio turinio sąrašui sukurti. Įterpiamas meniu pridedami apibrėžimai, teoriniai duomenys, įrodymai, pavyzdžiai, lentelės ir nuorodos. Pavyzdžiui:

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

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

Įrodymo langelis pateikia argumentą; priimtas Lean patikrinimas pateikia patikros ženklą. Pridėti šaltinius ir pasirinktines LaTeX makros po redaktoriumi, arba nustatyti nutylėjimą Jūsų profilis. Pasirinkite temą ir žymės, kad suinteresuoti skaitytojai gali rasti savo pranešimą.

Paskelbta pranešimai turi Redaguoti pranešimą nuorodą. Išsaugoti redagavimas lieka privatus, kol jūs skelbiate atnaujinimą. Straipsnis išsaugo savo adresą, ir esami mašinos patikrinimai lieka susieti su tekstu jie patikrino.

Toliau skaitykite kartu

Įrašyti pranešimus į savo privatų skaitymo sąrašą ir sekti autorius ar temas asmeniniam Toliau pateikta informacija pašarų. Atsakymai į savo pranešimus ir komentarus yra Atsakymai.

Sukurti knygą ar serijas Prijungti savo paskelbtus pranešimus. Pridėti skyrius, organizuoti savo užsakymą, ir padaryti turinį viešai, kai yra paruoštas. Privačios kolekcijos slepia savo turinį sąrašą; jos pranešimai lieka skelbiami individualiai.

Ženklas

∎ yra vadinamas halmos, po Paul Halmos, kuris pristatė pabaigos nepažeistas simbolis. Tai vienintelis dalykas šioje svetainėje, kad vykdo įgaliojimus, todėl sąmoningai sunku gauti:

• Tik Lean gali nustatyti. Išsamus spausdinimas True yra įrodymai, o ne įrodymai.
• sorry, native_decide, a šviežia axiom, unsafe ir debug.skipKernelTC atmetami anksčiau failas veikia, todėl apgavikas negali net išleisti kompiute.
• Vykdyti yra prisegtas prie tikslio teksto, kad jį. Redaguoti pranešimą ir ženklas eina įstrigęs, o ne perkelti į naujus žodžius.
• Jei tikrintojas yra žemyn, jūs gaunate "nepavyko paleisti", niekada "atmesta". Tikrintojo statusas dėl šios priežasties yra vieša.

Bendruomenės

Tikrinimas yra pigus; atradimas nėra. Bendruomenės yra bendras fondas apskaičiuoti, kad grindis atvirų problemų, ši valdyba balsavo iki. Kiekvienas gali prisidėti prie jo, niekas turi rezultatą, ir kiekvienas paleisti ji lėšos yra viešas, įskaitant tuos, kurie gavo niekur, kurie paprastai yra informatyvus.

Kas jį valdo

Halmos yra nepriklausomas ir mažas. Jei kas nors čia ne taip, greičiausias būdas tai įrodyti yra blokas, kurį serveris gali paleisti. Susisiekite.