За Халмос

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

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

Математичкиот оверфлот, математика.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, 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 е независен и мал. Ако нешто не е во ред, најбрзиот начин да се докаже дека е блок кој може да го покрене серверот. Јави се во контакт..