Про Halemos

Halmos - це дошка для математики, де сервер перевіряє математику. Здається, що будь- яке посилання на запис, аж доки ви не помітите, що деякі дописи не мають жодної суми, яку можна було б прочитати з упевненістю.

Проблема з кожним іншим форумом математики.

MathOverflow, math. StackExchange, r/ math, розділи коментарів arXiv. Всі вони мають лише один інструмент правильності: інші люди, аргументують. Це чудово працює, і тому неправильний доказ плавно перекреслює правильний текст, і чому " я перевіряв " і " Я вірю, що він " виглядає ідентичним на сторінці.

Halmos додає другий арбітролер, з яким неможливо сперечатися.

Що насправді робить сервер

Покладіть блок з загородою на будь-який пост або коментар, і він працює тут, при підданні:

Вивід, показаний під блоком, є тим, що інструмент друкував, дослівно. Ніколи не резюме: резюме точно є місцем, де буде вставлено в основу.

Як це зробити за хвилину

1. Коментарі зазвичай. Більшість дописів взагалі не мають математичних даних, а тут нічого не потрібно.
2. Записати математичні дані в тілі на $…$, або блок показу з $$…$$. Він передає як реальні математичні розрахунки; нічого не виконується. Це просто запис. побачити одного
3. Запитай машину. Обранено блок з міткою sage, gp, z3 або python виконується тут і вивід, який буде долучено до вашого допису, дослівно. Це не доказ, а доказ. побачити одного
4. Намалювати щось з a plot блок (matplotlib, з plt і np готовий), або визначити послідовність з oeis: вставте цілі числа, і вони повертаються до назви, якщо вона відома.
5. Доведи щось. А lean block перевіряється типом у математичному файлі. Вставте це у будь- який коментар: побачити одного

```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.
:::

У полі підтвердження буде показано аргумент; у полі для перевірки направа міститься позначка " Лівер." Додати джерела і нетипові макроси LaTeX під редактором або встановити типові значення у ваш профіль. Оберіть тему і мітки, які допоможуть вам знайти потрібний матеріал.

На опублікованих дописах міститься посилання Редагувати допис. Збережені зміни залишаться конфіденційними до того часу, коли ви оприлюднюватимете оновлення. У статті зберігається її адреса, а існуючі перевірки не зміняться на текст, який вони вказали.

Продовжуйте разом читати

Зберегти дописи до вашого особистого списку читання і стежити за авторами або темами для особистого Надалі fise. Відповіді на ваші дописи і коментарі з' являються у Відповіді вам.

Створити книгу або серію Щоб з' єднати ваші опубліковані дописи. Додайте розділи, влаштуйте їх порядок і оприлюдніть вміст, коли ви готові. Особиста збірка ховає список вмісту ваших дописів; її дописи не розкриваються окремо.

Позначка

∎ називається a 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:

• Лише Lean може встановити його. Друк дам True є доказ, не доказ.
• sorry, native_decide, новий axiom, unsafe і debug.skipKernelTC відкидається до файл запущено, отже, не можна навіть обчислювати.
• Виконання буде прив' язано до тексту, який його створив. Редагувати допис - не буде, а позначення не буде перенесене до нових слів.
• Якщо вас омине шашки "неможливо запустити", ніколи "відмовлено". Стан перевірки тому і публічно.

Громадяни

Перевірка дешева, а відкриття - ні. Громадяни є спільним пакетом обчислень, який підриває проблеми, які було проіснуто у цій дошці. Будь- хто може зробити свій внесок до неї, ніхто не володіє результатом, а всі його кошти - публічними, зокрема ті, які не мають доступу, які зазвичай є інформативними.

Хто заправляє

Halmos є незалежним і невеликим. Якщо щось у цьому випадку не так, найшвидший спосіб довести, що це блок, який може запустити сервер. Зв'яжіться.