เกี่ยวกับฮาลโมส

Halmos เป็นบอร์ดสำหรับคณิตศาสตร์ ที่เซิร์ฟเวอร์ตรวจสอบคณิตศาสตร์ มันดูเหมือนกับเครื่องรวบรวมลิงก์ จนกว่าคุณจะสังเกตเห็นว่า บางโพสต์มีสัญลักษณ์ที่แสดงว่า ไม่มีจำนวนการเขียนที่มั่นใจได้

ปัญหาของฟอรัมคณิตศาสตร์อื่นๆ

MathOverflow, math. StackExchange, r/math, arXiv comment sections ทุกอย่างมีผู้ตัดสินความถูกต้องเพียงคนเดียว: คนอื่นๆ ที่จะมาโต้แย้ง มันทำงานได้ดีมาก และมันก็เป็นเหตุผลที่ว่าทำไมการพิสูจน์ที่ผิดพลาดที่เขียนได้คล่องแคล่ว จะขึ้นอันดับสูงกว่าการพิสูจน์ที่ถูกต้องที่เขียนได้ไม่ดี และทำไม "ฉันตรวจสอบมัน" และ "ฉันเชื่อมัน" ดูเหมือนกันบนหน้า

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

การสมัครใช้บริการ ใช้ชื่อผู้ใช้และรหัสผ่าน ไม่มีอีเมล ไม่มีขั้นตอนการยืนยัน ทุกอย่างที่ผู้ตรวจสอบทำในขณะนี้ รอคิวและสถานะของผู้ตรวจสอบแต่ละคน หน้าสถานะถ้ามีคนหนึ่งตกลงมา คุณจะได้รับคำบอก "ไม่สามารถทำงาน" ไม่มี "ปฏิเสธ"

เขียนตามจังหวะของคุณ

เริ่มการโพสต์ และเปลี่ยนระหว่างการเขียนและดูก่อนอ่าน เพื่อดูคณิตศาสตร์ของคุณ เหมือนกับผู้อ่านจะเห็น การเปลี่ยนแปลงจะถูกบันทึกอัตโนมัติ ฉบับร่างของคุณการบันทึกร่างจะทำงานโดยไม่ต้องใช้จาวาสคริปต์ ส่วนร่างและตัวอย่างจะไม่ทำการประมวลผลโค้ด โปรดจัดพิมพ์เมื่อคุณพร้อมที่จะแบ่งปัน

ใช้หัวเรื่องเพื่อสร้างรายการเนื้อหาของบทความ เมนู แทรก จะเพิ่มคำนิยาม ทฤษฎี การพิสูจน์ ตัวอย่าง ตาราง และลิงก์ ตัวอย่างเช่น:

:::theorem Squares
For every real $x$, we have $x^2 \geq 0$.
:::

:::proof
Explain your argument here.
:::

กล่องพิสูจน์แสดงอาร์กิวเมนต์; การตรวจสอบ Lean ที่ยอมรับจะให้สัญลักษณ์การตรวจสอบ เพิ่มแหล่งข้อมูลและมาโคร 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 เป็นอิสระและเล็ก ถ้ามีบางอย่างที่นี่ผิด วิธีการที่รวดเร็วที่สุดเพื่อพิสูจน์มันคือ บล๊อกเซิร์ฟเวอร์สามารถทำงาน ติดต่อมา.