Дар бораи Халмос

Halmos - ин ҷадвали математика мебошад, ки дар он сервер математикаро тафтиш мекунад. Ин ба монанди ягон алоқаи ҷамъкунанда ба назар мерасад, то он даме, ки шумо мушоҳида кунед, ки баъзе гузоришҳо нишонаи навиштани бовариро надоранд.

Масъала бо ҳар як форуми дигари математика

MathOverflow, math.StackExchange, r/math, arXiv шарҳҳои қисмҳо. Ҳама аз онҳо танҳо як арбитри дурустӣ доранд: дигар одамон, баҳс. Ин хеле хуб кор мекунад, ва ин ҳам сабаби он аст, ки исботи хато навишташудаи хуб аз он хатои навишташудаи дуруст боло меравад, ва чаро "Ман онро санҷидам" ва "Ман ба он бовар дорам" дар саҳифаи якхела ба назар мерасанд.

Halmos як арбитри дуюмро илова мекунад, ки бо он баҳс кардан мумкин нест.

Чӣ кор мекунад сервер

Ба ҳар як мақолот ё шарҳ блоки муҳофизатшударо гузоред ва он дар ин ҷо, ҳангоми фиристодан иҷро мешавад:

Баромадани нишондодашуда дар зери блок ин аст, ки асбоб чоп кардааст, ба таври дуруст. Ҳеҷ гоҳ ҷамъбаст: ҷамъбасткунӣ дар он ҷое, ки истеҳсолот ба он ҷо мегузарад.

Чӣ тавр онро санҷед, дар як дақиқа

1. Шарҳи оддӣ. Бисёре аз мақолотҳо дар худ ягон математикаро надоранд ва дар ин ҷо ягон чизро талаб намекунанд. Ҷавобҳо дар анбор.
2. Матнҳои математикӣ бо $…$, ё блоки намоиш бо $$…$$. Он ҳамчун матнҳои математикии воқеӣ тасвир мекунад; ҳеҷ чиз иҷро намешавад. Ин танҳо аломатгузорӣ аст. якто
3. Аз мошин пурсед. Блоки аломатдор sage, gp, z3 ё python Дар ин ҷо иҷро карда мешавад ва натиҷаи он ба мақолоти шумо пайваст карда мешавад. Ин далел аст, на далел. якто
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, баъди Пол Halmos, ки нишонаи охиринро барои исбот ворид кард. Ин танҳо чизест, ки дар ин сайт мавҷуд аст, ки ба он иҷозат медиҳад, бинобар ин, ба таври ихтиёрӣ душвор аст, ки ба даст оред:

• Танҳо Lean метавонад онро танзим кунад. Чопи Sage True Ин гувоҳӣ аст, на далел.
• sorry, native_decide, нав axiom, unsafe ва debug.skipKernelTC рад карда шудаанд пеш аз файл иҷро мешавад, аз ин рӯ, фишанг ҳатто ҳисобкуниро сарфа карда наметавонад.
• Дар ин ҳолат, барои ҳар як аломати нав, матни нав эҷод карда мешавад. Агар шумо мақолотро таҳрир кунед, аломати нав ба ҷои гузаронидани калимаҳои нав, кӯҳна мешавад.
• Агар як шоҳ аз поён бошад, шумо мегиред "иҷро карда натавонист", ҳеҷ гоҳ "рад карда шуд". Санҷиши ҳолати система Ин барои ҳамин сабаб оммавӣ аст.

Муштариён

Ин раванди гузариш аз ибтидоӣ ба ниҳоятӣ ном дорад. Муштариён Ин як ҷамъи компютерӣ мебошад, ки дар масъалаҳои кушодаи ин тахта овоз додааст. Ҳар кас метавонад ба он саҳмгузорӣ кунад, ҳеҷ кас соҳиби натиҷа нест, ва ҳар як иҷрои он маблағгузорӣ мешавад, аз ҷумла онҳое, ки ба ягон ҷо нарафтанд, ки одатан онҳое, ки иттилоотӣ мебошанд.

Кӣ онро иҷро мекунад

Halmos мустақил ва хурд аст. Агар дар ин ҷо ягон чизе хато бошад, роҳи тезтарини исбот кардани он блокест, ки сервер метавонад иҷро кунад. Дар тамос шавед.