Halmos Hakkynda

Halmos bir matematika üçin tabldyr, serwer matematikany barlaýar. Bu her bir baglanyşyk aggregatory ýaly görünýär, siz käbir makalalaryň hiç bir ätiýaçly ýazmak mukdaryny döredip bilmeýän bir nyşany barlaýança.

Her bir beýleki matematika forumy bilen problema

MathOverflow, math.StackExchange, r/math, arXiv kommentari bölümleri. Olaryň hemmesi dogrylyk üçin bir arbiter bar: beýleki adamlar, gürleşip. Bu gowy işleýär, we bu hemme sebäbi ýalňyş ýazylan subutnamaň dogry ýazylany betereňleşdirýär, we sebäbi "Men ony barladym" we "Men oňa ynandym" sahypada birmeňzeş görünýär.

Halmos ikinji arbiter ekleýär bu bilen gürleşip bolmaýar.

Serweriň hakykatda näme edýändigi

Her bir makala ýa-da kommentariýa içine bir blok goý we ol şu ýerde işleýär, iberilende:

Bir blok astynda görkezlen çykdajy esbap çap eden zat, sözme söz. Hiç wagt bir jemle: jemlemek dogry bir fabbrikasiýa girip gidýän ýeridir.

Ony nädip synlamaly, bir minutda

1. Normal kommentari Çokly postlar olarda hiç matematiki bar we hiç zat bu ýerde hiç bir matematiki gerek etmeýär.
2. Matematikany hatda ýaz bilen $…$, ýa-da bir görkezme bloky bilen $$…$$. Bu akyly reňk taýýarlama reňklemedir; hiç zat işlenilmez. Bu diňe notatsiya. bir gör
3. Maşyndan sora Bir tagly blok sage, gp, z3 ýa-da python bu iş şu ýerde ýerine ýetirilýär we onuň çykdajylary siziň poçtuňyza goşulýar, sözme-söz. Bu subutnama, subutnama däl. bir gör
4. Bir zady suratlandyr bir plot blok (matplotlib, bilen plt we np _Gün tertibini görkez oeis: tagtlary goyp we ol adyny getirip, eger belli bolsa.
5. Bir zady subut et A lean blok Mathlib bilen tip barlaýar. Şuny her bir kommentariýa goýdyň: bir gör

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

Signing up is a username and a password: no email, no confirmation step. Everything the checkers are doing right now is on the gapy, we her bir barlaýanyň ýaşaýan ýagdaýy şu ýerdedir status page: eger bir aşak bolsa size "işletmek başarmady" diýilýär, hiç wagt "rejected" diýilmez.

Özüň ýaz

Bir makala başla we ýazmak we öň görmek arasyny aýla we matematikiňi okaýanlar ýaly gör. üýtgemeler otomatik gaýd edilsin Siziň draftlaryňyz; Gaýd et çakyrlygy JavaScriptsiz hem işleýär. Çakyrlyklar we öň görüşler hiç wagt kod işletmez. Paýlaşmaga taýýar bolanda çap et.

Meňzeş bir maqaleň mazmuny taryhyny düzmek üçin başlyklardan peýdalan. Ekle menüsi düşündirmeleri, teoremleri, subutnamalary, mysallary, täblisalary we baglanyşyklary goşýar. Meselem:

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

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

Bir subut pökgüsi bir argümenty görkezýär; kabul edilen Lean barlagyny barlagyň nyşanyny berer. çeşmeleri we öz LaTeX makrolary redaktoryň astyna ekle, ýa-da öň bellenenleri belle profil. Bir mesel we tagy saýlaň, şeýlelik bilen gyzyklanýan okyjylar siziň makalaňyzy tapyp bilerler.

Published posts have an Edit post link. Saved edits remain private until you publish the update. The article keeps its address, and existing machine checks stay tied to the text they checked.

Birleşik okama

Açar sözleri şahsy okamak sanawyna gaýd et we awtorlary ýa-da temalary şahsy bir zat üçin yzarla _Aşak feed. Your posts and comments responses appear in Saňa jogaplar.

Bir kitap ýa-da seriýa bejer Öz çap edilen makalalaryňy baglamak üçin. Faýllary ekle, olary tertibe sal we mazmuny taýyn bolanda açyk et. Özel bir toplama öz mazmunyny gizleýär; öz makalalary özbaşdak çap edilşini saklaýar.

Mark

∎ a halmos, after Paul Halmos, who introduced the end- of- proof symbol. It's the only thing on this site that carries authority, so it's deliberately difficult to get:

• Sage çapla True bu bir subutnama, däl-de bir subutnama.
• sorry, native_decide, bir axiom, unsafe we debug.skipKernelTC ret edildi öň faýl işleýär, şonuň üçin bir çit haçan-da hasap edip bilmez.
• Bir öwürmek ony döreden metinde öwürilýär. Edebiň edit edilip we nyşan täze sözlere geçilmekden başga gadymlaşyp gidýär.
• Eger bir çep aşakda bolsa siz alarsyňyz "işlenip tamamlanmady", hiç wagt "ret edildi". _Gün tertibi bu sebäpden halka aýan.

Umumy

Barlaňkylyk gymmatly; tapmak gymmatly däl. Umumy bu bir paylaşylan kompýuter ätiýaçlyky bu borduň ses beren açyk meselelerini işleýän. Her kim oňa goşant goşyp biler, hiç kim netijä eýelik etmez we her bir işleýän fonlary halkydyr, hiç ýere gitmedikleri hem içer, olar adatça maglumatlylar.

Ony kim işledýär

Halmos özbaşdak we kiçi. Eger bir zat bu ýerde hataly bolsa, iň tiz ýoly serweriň işledip biljek bloky görkezmekdir. Baglanyşyk.