О Халмосу
Halmos је табла за математику где сервер проверава математику. Изгледа као да је било ко агрегатор повезања док не приметите да неки постови не носе знак који не може да произведе количина самоувереног писања.
Проблем са свим другим форумом математике
Математички оверфлот, математика. СтацкЕкспомен, r/math, arXiv коментар секције. Сви они имају тачно један арбитер исправности: други људи, свађају се. То ради изузетно добро, а то је и разлог зашто погрешан доказ течно надмашује исправну писану, а зашто "ја сам га проверио" и "Верујем да" изгледа идентично на страници.
ЗHalmos додаје други арбитер са којим се не може расправљати.
Шта сервер заправо ради
Ставите ограду блок у било којем посту или коментару и ради овде, на подношење:
| Блок | Шта се дешава | Може ли да заради ∎? |
|---|---|---|
lean |
Пров› јерено против Матлиба. Језгро прихвата доказни израз или не. | Да. |
sage | Сагемат га води; прави излаз је прикачен на посту. | Не |
gp | ПАРИ/ГП га води. | Не |
z3 | З3 тражи модел: најбржи начин за Побијегни Нешто. | Не |
python | Питон у пешчаном сандуку, прикачен излаз. | Не |
Излаз који се приказује испод блока је штампана алатка, дословно. Никада сажетак: сажетак је тачно место где би се измишљање увукло.
Како да пробам, за минут
- Коментирај нормално. Већина положаја нема математике у њима уопште и ништа овде не захтева никакво.
- Упиши у графику математике са
$…$, или приказни блок са$$…$$. Исцртава као праву математику типа; ништа се не извршава. То је само запис. Види један - Питај машину. Оградени блок означен
sage,gp,z3илиpythonОвде је извршен и његов излаз је прикачен на ваш пост, дословно. Види један - Нацртај нешто са
plotблок (матплотлиб, саpltиnpспреман), или идентификуј низ саoeis: налепите целе бројеве и враћа се именом, ако је познато. - Докажи нешто. А
leanблок је пров› јерен према Матлибу. Налепи ово у било који коментар: Види један
```lean
import Mathlib
theorem two_add_two : 2 + 2 = 4 := by norm_num
```
Потписивање је корисничко име и лозинка: без е‐ поште, без корака потврде. Све што даме сада раде је на ред, и сваки чекер је жива стање је на стање странице: ако је један доле вам је речено "не може да покрене", никада "одбијен".
Пиши својим темпом.
Покрени пост и пребацивање између писања и прегледа да бисте гледали математику као читаоце. Изм› јене су аутоматски уписиване у Ваш нацртСачувај нацрт такође ради без ~@ ¦јаваскрипта¦JavaScripta¦. Нацртови и прегледи никада не покрећу код. Објављуј када сте спремни да га поделите.
Заглавља за израду списка садржаја чланка. Мени Уметни дефиниције, теореме, доказе, примере, табеле и везе. На пример:
:::theorem Squares
For every real $x$, we have $x^2 \geq 0$.
:::
:::proof
Explain your argument here.
:::
Доказан поље представља аргумент; прихватена провера за оверу додаје знак. Додај изворе и посебне ~@ ¦Летекс¦LaTeX¦ макрое испод уређивача, или подразум› ијевано у ваш профил. Изаберите тему и ознаке тако заинтересовани читаоци могу да нађу свој пост.
Објављене поруке имају везу уређивања поште. Уређивање сачувано остаје приватно док не објавите ажурирање. Чланак чува адресу, а постојеће пров› јерења на машини остају везани за текст који су утврдили.
Настави да читаш заједно
Сачувај постове на приватну листу читања и прати ауторе или теме за личну Прати довод. Одговори на ваше постове и коментаре се појављују у Одговори теби.
Направи књигу или серије да повежете објављене постове. Додајте поглавља, организујте њихов редослед и објавите садржај када будете спремни. Приватна збирка сакрива списак садржаја, њени послови остају објављени појединачно.
Знак
∎ Зове се halmos, after Paul Halmos, who introduced the end-of-proof symbol. It is the only thing on this site that carries authority, so it is deliberately hard to get:
- Само Лиан може да га постави.
Trueје доказ, није доказ. sorry,native_decide, свежaxiom,unsafeиdebug.skipKernelTCодбијају се пре Фајл ради, тако да преварант не може ни да потроши рачуне.- Покретање је прикачено на тачан текст који га је произвео. Уредите положај и знак ће устајати, а не пребацивати на нове речи.
- Ако је провера доле, добијеш "не могу да покренем", никада "одбијен". Стање контроле је јавно из тог разлога.
Заједница
Провера је јефтина; откриће није. Заједница Свако може да допринесе резултату, нико не поседује резултат, а сваки пролаз је јаван, укључујући и оне који су ничему нестали, који су обично информативни.
Ко га води
Halmos је независан и мали. Ако нешто није у реду, најбржи начин да се докаже је блок који сервер може да покрене. Јави се..