Halmos ∎

О Халмосу

Halmos је табла за математику где сервер проверава математику. Изгледа као да је било ко агрегатор повезања док не приметите да неки постови не носе знак који не може да произведе количина самоувереног писања.

Проблем са свим другим форумом математике

Математички оверфлот, математика. СтацкЕкспомен, r/math, arXiv коментар секције. Сви они имају тачно један арбитер исправности: други људи, свађају се. То ради изузетно добро, а то је и разлог зашто погрешан доказ течно надмашује исправну писану, а зашто "ја сам га проверио" и "Верујем да" изгледа идентично на страници.

ЗHalmos додаје други арбитер са којим се не може расправљати.

Шта сервер заправо ради

Ставите ограду блок у било којем посту или коментару и ради овде, на подношење:

БлокШта се дешаваМоже ли да заради ∎?
lean Пров› јерено против Матлиба. Језгро прихвата доказни израз или не. Да.
sageСагемат га води; прави излаз је прикачен на посту.Не
gpПАРИ/ГП га води.Не
z3З3 тражи модел: најбржи начин за Побијегни Нешто.Не
pythonПитон у пешчаном сандуку, прикачен излаз.Не

Излаз који се приказује испод блока је штампана алатка, дословно. Никада сажетак: сажетак је тачно место где би се измишљање увукло.

Како да пробам, за минут

  1. Коментирај нормално. Већина положаја нема математике у њима уопште и ништа овде не захтева никакво.
  2. Упиши у графику математике са $…$, или приказни блок са $$…$$. Исцртава као праву математику типа; ништа се не извршава. То је само запис. Види један
  3. Питај машину. Оградени блок означен sage, gp, z3 или python Овде је извршен и његов излаз је прикачен на ваш пост, дословно. Види један
  4. Нацртај нешто са plot блок (матплотлиб, са plt и np спреман), или идентификуј низ са oeis: налепите целе бројеве и враћа се именом, ако је познато.
  5. Докажи нешто. А 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 је независан и мали. Ако нешто није у реду, најбржи начин да се докаже је блок који сервер може да покрене. Јави се..

Придружи се разговору.

Упишите се да пишете, сачувате идеје, и пратите људе који вас инспиришу.

Направи налог · Заборавио лозинку?

Корисничко име и лозинка су све што треба да почнете.

Пошаљи нам повратну информацију

Реци нам шта се десило или шта си очекивао.

Ако си оставио имејл, одговорићемо.