Халмос

Halmos нь математикийн сервер нь математикийн шалгалт хийдэг математикийн форум юм. Энэ нь холбоос цуглуулагч шиг харагдаж байгаа боловч зарим нийтлэлүүд нь ямар ч бичлэг бичих чадваргүй гэсэн тэмдэглэгээтэй байдаг.

Бусад математикийн форумуудын асуудал нь

MathOverflow, math.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 макрог редакторын доор нэмж, эсвэл стандартыг тохируулна уу. Таны профайл. Choose a subject and tags so interested readers can find your post.

Нийтлэгдсэн нийтлэлд Нийтлэлийг өөрчлөх холбоос байдаг. Та шинэчлэлийг нийтлэхгүй бол хадгалсан өөрчлөлтүүд нууц хэвээр үлдэнэ. Мэдээ нь хаягаа хадгалж, машин дээрх шалгалтууд нь шалгасан тексттэй холбоотой үлдэнэ.

Хамтдаа уншина уу

Таны хувийн уншлагын жагсаалтад нийтлэлүүдийг хадгалж, зохиогч эсвэл сэдвийг дагана Дараа нь Хуваалцах мэдээ. Таны нийтлэл, сэтгэгдэлд хариулах нь энэ хэсэгт харагдана. Танайд хариулах.

Ном эсвэл цуврал үүсгэх Таны нийтлэгдсэн нийтлэлүүдийг холбох. Хэсэгүүдийг нэмж, дарааллыг нь тохируулж, бэлэн болмогц агуулгыг нийтэд нээлттэй болгоно. Хувийн цуглуулга нь агуулгаа нууж, нийтлэлүүд нь тусгайлан хэвлэгдсэн хэвээр байна.

Үг

∎ гэж нэрлэдэг halmos, Paul Halmos- ийн нэрээр, баталгааны төгсгөлийн тэмдэгтийг танилцуулсан. Энэ нь энэ сайт дээрх ганцхан дүгнэлттэй зүйл бөгөөд үүнийг олоход хэцүү:

• Зөвхөн Lean л үүнийг тохируулж чадна. Sage хэвлэх True Энэ нь нотлох баримт биш, баталгаа юм.
• sorry, native_decide, шинэ axiom, unsafe ба debug.skipKernelTC үгүйсгэгдсэн өмнө файл нь ажиллана, тиймээс хууран мэхлэгч тооцоолол зарцуулахгүй.
• Үйлдэл нь түүнийг үүсгэсэн яг тэрхүү бичлэгт хадгалагдана. Хэрэв бичлэгийг өөрчлөхөд шинэ үгс рүү шилжихээс илүүтэй тэмдэглэгээ нь хуучирна.
• Хэрэв та хэрэв нэг даалгавар нь доош бол "гүйцэтгэх боломжгүй", хэзээ ч "үгүйсгэсэн". Бүтэцийг шалгах энэ шалтгааны улмаас нийтийн юм.

Нийтлэг

Шалгах нь хямд, олж илрүүлэх нь үнэтэй. Нийтлэг Энэ нь энэ зөвлөлийн санал болгосон нээлттэй асуудлыг шийдэх тооцооллын нийтлэг сан юм. Хэн ч оролцож болно, хэн ч үр дүнг эзэмшдэггүй, бүх үйлдлийн санхүү нь нийтэд нээлттэй, мэдээллийн зорилгоор хийгдсэн, ямар ч үр дүнгүй үйлдлүүдийг ч багтаасан.

Хэн удирддаг вэ?

Halmos нь тусгаарлагдсан ба жижиг. Хэрэв энд ямар нэгэн алдаа гарвал, серверийн гүйцэтгэх блок нь үүнийг батлах хамгийн хурдан арга юм. Харилцаарай.