Halmos жөнүндө

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 макросы добавьте в редакторе или установите предпочтения в профилиңизТеманы жана тегдерди тандаңыз, ошондо кызыккан окурмандар сиздин макалаңызды таба алышат.

Опубликованое сообщение имеет ссылку Изменить сообщение. Сохраненные изменения остаются частными до тех пор, пока вы не опубликуете обновление. Статья сохраняет свой адрес, а существующие машинные проверки остаются связанными с текстом, который они проверяли.

Бирге окуйбуз

Публикации в личном списке чтения и просмотр авторов или тем для личного пользования Кийинки Сиздин билдирүүлөргө жана комментарийлерге жооптор төмөнкүдөй көрсөтүлөт: Сизге жооп.

Китеп же серияны жаратуу Публикацияны бириктирүү үчүн. Часть добавить, расставить их по порядку и сделать содержание открытым, когда оно готово. Частная коллекция скрывает свой список содержания, а публикации остаются индивидуальными.

Белги

∎ деп аталат halmos, Paul Halmos аттуу адам тарабынан, ал далилдин аягына карата символду киргизген. Бул сайтта авторитеттүү болгон бир гана нерсе, ошондуктан аны алууну ойлоп табуу кыйын:

• Аны жөн гана Lean орното алат. Sage басып чыгаруу True Бул далил, далил эмес.
• sorry, native_decide, жаңы axiom, unsafe жана debug.skipKernelTC кабыл алынбайт мурун файл аткарылат, ошондуктан шылуундук эсептөөгө да жумшабайт.
• Тексттик файлды жүктөп алууда, ал тексттик файлды түзгөн текстке гана фиксирленет. Эгерде сиз макаланы өзгөртсөңүз, анда жаңы сөздөргө которулбай, эскирген текстке гана фиксирленет.
• Эгерде шашка ылдый болсо, сизди "аткарууга болбоду", эч качан "четке кагылган". Статус текшергичи бул себептүү ачык.

Коммьюнити

Текшерүү арзан, бирок ачылыш арзан эмес. Коммьюнити бул бул панелдин добуш берген ачык маселелери боюнча иштелип чыккан жалпы эсептөө фонду. Ар ким ага салым кошо алат, эч ким жыйынтыктын ээси эмес, жана ар бир аткаруу үчүн каражат ачык, анын ичинде эч жакка чыкпагандар, алар адатта маалыматтык.

Аны ким иштетет

Halmos - это независимый и маленький файл. Если здесь что-то не так, то это можно быстро доказать, выполнив блок на сервере. Байланыш.