За Халмос
Halmos е дъска за математика, където сървъра проверява математиката. Изглежда като всяка връзка агрегатор, докато забележите, че някои публикации не носят маркира, без самоуверено писане може да произвежда.
Проблемът с всеки друг форум по математика
MathOverflow, математика.StackExchange, r/math, arXiv коментар секции. Всички те имат точно един арбитър на правилност: други хора, спорещи. Това работи забележително добре, и това е също защо погрешно доказателство, пишан течно надхвърля правилния написан лошо, и защо "Аз го проверих" и "Вярвам, че" изглеждат идентични на страницата.
Halmos добавя втори арбитър, с който не може да се спори.
Какво всъщност прави сървърът
Поставете ограден блок във всеки пост или коментар и той работи тук, при подаване:
| Блок | Какво става? | Може ли да спечели? ∎? |
|---|---|---|
lean |
Type-checked against Mathlib. The kernel accepts the proof term or it does not. | Да. |
sage | SageMath го управлява; реалното изходно е прикрепено към поста. | Не. |
gp | Пари/ГП го управлява. | Не. |
z3 | Z3 търси модел: най-бързият начин за опровергаване Нещо. | Не. |
python | Сандбоксиран Python, изход прикрепен. | Не. |
Изходът, показан под блок е това, което инструментът е отпечатан, дословно. Никога резюме: обобщаването е точно там, където се промъква изработката.
Как да опитаме, след минута
- Коментирайте нормално. Повечето публикации нямат математика в тях на всички и нищо тук изисква. Отговори гнездото.
- Напишете математика в редица с
$…$, или дисплей с блок$$…$$. Той прави като реална типографска математика; нищо не се изпълнява. Виж едно - Попитай машината. Ограден блок с маркирани
sage,gp,z3илиpythonе извършено тук и резултатът му е приложен към вашето място, дословно. Виж едно - Нарисувай нещо с
plotблок (матплотлиб, сpltиnpГотови), или идентифицират последователност сoeis: вмъкнете числата и тя се връща името, ако е известно. - Докажи нещо. А
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, който въведе крайната-устойчив символ. Това е единственото нещо на този сайт, което носи власт, така че е умишлено трудно да се получи:
- Само Лиан може да го настрои.
Trueе доказателство, не доказателство. sorry,native_decide, пряснаaxiom,unsafeиdebug.skipKernelTCсе отхвърлят преди файлът работи, така че мамката не може дори да изчисли.- Записът се прикрепя към точния текст, който го е направил. Редактиране на пощата и маркировката става застаряла, вместо да прехвърля на нови думи.
- Ако е свалена чеката, ще получиш "не може да се изпълни", никога "отхвърлено". Статус на контрола е публично по тази причина.
Общината
Проверката е евтина; откритието не е. Общината е общ басейн от изчисления, че меле на отворените проблеми този борд е гласувал. Всеки може да допринесе за него, никой не притежава резултата, и всеки пробег той средства е обществен, включително тези, които не са стигнали до никъде, които обикновено са информативните.
Кой го управлява?
Halmos е независим и малък. Ако нещо тук не е наред, най-бързият начин да се докаже, че това е блок, който сървърът може да изпълни. Свържи се с мен..