Halmos ҳақида

Halmos - бу сервер математикани текширадиган математика учун тахта. У баъзи мақолалар ишончли ёзиш учун етарлича бўлмаган белгини олиб келишини сезгунингизча, у бошқа бирор алоқа йиғувчисига ўхшайди.

Ҳар бир бошқа математика форумидаги муаммо

MathOverflow, math.StackExchange, r/math, arXiv шарҳлар бўлими. Уларнинг барчасида тўғриликнинг биргина арбитри бор: бошқа одамлар, баҳслашаётганлар. Бу жуда яхши ишлайди, бу ҳам тўғри ёзилган хато исботнинг ёмон ёзилган тўғри исботдан юқорироқ ўринга эга бўлишининг сабаби, ва "Мен текширдим" ва "Мен ишонаман" саҳифада бир хил кўриниши сабабидир.

Halmos билан баҳслашилмайдиган иккинчи арбитрни қўшиб қўяди.

Сервернинг асл вазифаси

Ҳар қандай мақола ёки шарҳга ўралган блокни қўйинг ва у бу ерда, тақдим этилганда ишлайди:

Блок остида кўрсатилган чиқим асбоб чоп этган нарса, сўзма-сўз. Ҳеч қачон қисқача: қисқача аниқ бир ишлаб чиқаришни киритиш учун.

Уни қандай синаш мумкин, бир дақиқада

1. Оддий шарҳ. Кўпгина постларда математика умуман йўқ ва бу ерда ҳам ҳеч нарса математикани талаб қилмайди.
2. Математикларни ёзиш билан $…$, ёки экран блоки билан $$…$$. У ҳақиқий матн матнлари каби кўрсатилади; ҳеч нарса бажарилмайди. Бу фақат нот. бир кўринг
3. Машинадан сўранг. Эгилган ўралган блок sage, gp, z3 ёки python is executed here and its output attached to your post, verbatim. That is evidence, not proof. бир кўринг
4. Нимадир чизинг билан plot блок (matplotlib, билан plt ва np тайёр), ёки кетма-кетликни бу билан аниқланг oeis: тўлиқ сонларни жойлайди ва агар маълум бўлса, номланган ҳолда қайтаради.
5. Бирор нарсани исботла. А lean блок Mathlib билан тип текширилган. Буни ҳар қандай изоҳга жойланг: бир кўринг

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

Роҳхатдан ўтиш фойдаланувчи номи ва махфий сўз билан амалга оширилади: электрон почта йўқ, тасдиқлаш қадами йўқ. Ҳозирда текширувчилар қилаётган барча ишлар навбат, ва ҳар бир текширувчининг жонли ҳолати саҳифа: агар бирортаси паст бўлса, сизга "йўлланмади" дейилади, ҳеч қачон "тақиқланмади".

Ўзингиз ёзинг

Мақола бошлаш ва матнни ёзиш ва матнни кўриш ўртасида ўтиш учун матнни ўқиб кўргандек кўришингиз мумкин. Ўғирликлар автоматик тарзда сақланадиган жой Сизнинг лойиҳаларингиз; Драфтни сақлаш JavaScriptсиз ҳам ишлайди. Драфт ва кўринишлар ҳеч қачон кодни бажармайди. Уни ўртоқлашишга тайёр бўлганингизда эълон қилинг.

Мақоланинг мазмунини тузиш учун сарлавҳалардан фойдаланинг. Қўшиш менюси тушунчалар, теоремалар, исботлар, мисоллар, жадваллар ва алоқаларни қўшиб беради. Мисол учун:

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

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

Ҳужжат қутиси аргументни тақдим этади; қабул қилинган Lean текшируви текшириш белгисини тақдим этади. Манбаларни ва LaTeX макросларини редактор остида қўшинг ёки олдинги ҳолатни ўрнатинг профилингизМавзу ва теги танланг, шунинг учун қизиққан ўқувчилар мақолангизни топа оладилар.

Чоп этилган мақолалар мақолани таҳрирлаш ҳаволасига эга. Сақланган ўзгартиришлар янгиланишни эълон қилганингизгача махфий қолади. Мақола ўз манзилини сақлаб қолади ва мавжуд машина текширувлари улар текширган матнга боғланган қолади.

Бирга ўқиб боринг

Мақолаларни шахсий ўқиш рўйхатига сақланг ва муаллифлар ёки мавзуларни шахсий кузатиш учун кузатинг Кейинги Feed. Сизнинг мақолаларингиз ва шарҳларингизга жавоблар бу ерда пайдо бўлади Сизга жавоблар.

Китоб ёки серия яратиш Чоп этилган мақолаларингизни боғлаш учун. Бобларни қўшиш, уларнинг тартибини белгилаш ва тайёр бўлганда мазмунни оммалаштириш учун. Шахсий тўплам ўз мазмунини яширади; унинг мақолалари алоҳида-алоҳида чоп этилади.

Марк

∎ деб номланади halmos, Paul Halmos дан кейин, у исботнинг охири белгисини киритган. Бу сайтдаги ягона ишончли нарса, шунинг учун уни олиш жуда қийин:

• Уни фақат Lean ўрнатиши мумкин. Sage чоп этиш True Бу далилдир, далил эмас.
• sorry, native_decide, янги axiom, unsafe ва debug.skipKernelTC рад қилинади олдин файл ишга туширилади, шунинг учун адаштирувчи ҳисоблашни сарфлай олмайди.
• Юклаш уни яратган матнга ёпиштирилади. Мақолани таҳрирлашда белги янги сўзларга кўчирилгандан кўра эскириб қолади.
• Агар чекка тушиб кетса, сиз олинг "ишга туширилмади", ҳеч қачон "рад этилди". Ҳолатни текшириш Унинг аҳлидандир.

Жамият

Буни Аллоҳ таоло Ўзи хоҳлаган кишиларга осон қиладир. Жамият бу бу режа овоз берган очиқ муаммоларни қирқиш учун ўртоқлашилган ҳисоблаш пули. Ҳар ким унга ҳисса қўшиши мумкин, натижа ҳеч кимга тегишли эмас ва ҳар бир ишга тушириш фонди очиқ, бунда ҳеч қаерга бормаганлар ҳам, одатда ахборотлилар ҳам киради.

Уни ким бошқаради?

Halmos мустақил ва кичик. Агар бу ерда бирор нарса хато бўлса, буни исботлашнинг энг тезкор йўли сервер ишга туширадиган блокдир. Алоқа ўрнатиш.