Về Halmos
Halmos là một bảng toán học nơi máy chủ kiểm tra toán học. Nó trông giống như bất kỳ tập hợp liên kết nào cho đến khi bạn nhận ra rằng một số bài viết có dấu hiệu không có số lượng viết tự tin có thể tạo ra.
Vấn đề với mọi diễn đàn toán học khác
MathOverflow, math.StackExchange, r/math, các phần bình luận arXiv. Tất cả chúng đều có chính xác một người phán xét về sự chính xác: những người khác, tranh luận. Điều đó hoạt động rất tốt, và đó cũng là lý do tại sao một chứng minh sai được viết một cách lưu loát hơn một chứng minh đúng được viết một cách tồi tệ, và tại sao "Tôi kiểm tra nó" và "Tôi tin nó" trông giống nhau trên trang.
Halmos thêm một trọng tài thứ hai mà không thể tranh luận với.
Những gì máy chủ thực sự làm
Đặt một khối rào trong bất kỳ bài viết hay bình luận nào và nó chạy ở đây, khi gửi:
| Kích thước | Chuyện gì sẽ xảy ra? | Có thể kiếm được ∎? |
|---|---|---|
lean |
Kiểm tra kiểu đối với Mathlib. Nhân chấp nhận thuật ngữ chứng minh hay không. | Có chứ. |
sage | SageMath chạy nó; kết quả thực tế được ghim vào bài viết. | Không |
gp | PARI/GP điều hành nó. | Không |
z3 | Z3 tìm kiếm một mô hình: cách nhanh nhất để từ chối cái gì đó. | Không |
python | Python sandboxed, kết quả gắn liền. | Không |
Kết quả xuất ra được hiển thị dưới một khối là những gì công cụ in ra, theo nghĩa đen. Không bao giờ là một tóm tắt: tóm tắt chính xác là nơi mà một sự chế tạo sẽ lộ ra.
Làm sao để thử nó, trong khoảng một phút
- Nói bình thường đi. Hầu hết các bài viết không có toán học nào cả và không có gì ở đây cần phải có toán học.
- Viết toán học vào dòng với
$…$, hoặc một khối hiển thị với$$…$$. Nó hiển thị như toán học thực sự; không có gì được thực hiện. Nó chỉ là ký hiệu. xem một cái - Hỏi máy. Một khối được gắn thẻ
sage,gp,z3hoặcpythonĐó là bằng chứng, không phải là chứng minh. xem một cái - Vẽ gì đó đi. với
plotkhối (matplotlib, vớipltvànpsẵn sàng), hoặc xác định một chuỗi vớioeis: dán các số nguyên và nó sẽ trở lại với tên, nếu nó được biết. - Chứng minh điều gì đó. A-M_BAR_Tiếng Anh (Mỹ)
leankhối được kiểm tra kiểu đối với Mathlib. Đưa vào bất kỳ ghi chú nào: xem một cái
```lean
import Mathlib
theorem two_add_two : 2 + 2 = 4 := by norm_num
```Đăng ký chỉ cần tên người dùng và mật khẩu: không cần email, không cần xác nhận. Mọi thứ mà các kiểm tra đang làm bây giờ đều nằm trên máy tính. hàng đợi, và trạng thái sống của mỗi người kiểm tra là trên Thư mụcNếu một cái bị hỏng, bạn sẽ được nói "không thể chạy", không bao giờ "bị từ chối".
Viết theo tốc độ của bạn
Đầu tư và chuyển đổi giữa viết và xem trước để xem toán học của bạn như người đọc sẽ xem. Các thay đổi tự động lưu vào Dự thảo của anh.; Lưu bản thảo cũng hoạt động mà không cần JavaScript. Bản thảo và xem trước không bao giờ chạy mã. Công bố khi bạn sẵn sàng chia sẻ.
Dùng tiêu đề để xây dựng danh sách nội dung của bài viết. Trình đơn Ghi vào thêm định nghĩa, định lý, chứng minh, ví dụ, bảng và liên kết. Ví dụ:
:::theorem Squares
For every real $x$, we have $x^2 \geq 0$.
:::
:::proof
Explain your argument here.
:::Một hộp chứng minh trình bày một đối số; một kiểm tra Lean chấp nhận cung cấp dấu kiểm tra. Thêm nguồn và macro LaTeX tùy chỉnh dưới trình biên tập, hoặc đặt mặc định trong hồ sơ của bạnChọn một chủ đề và một nhãn để người đọc có thể tìm thấy bài viết của bạn.
Bài đăng đã xuất bản có liên kết Sửa bài đăng. Các thay đổi đã lưu vẫn giữ bí mật cho đến khi bạn xuất bản cập nhật. Bài viết giữ địa chỉ của nó, và các kiểm tra máy hiện có vẫn liên kết với văn bản chúng kiểm tra.
Đọc tiếp đi.
Lưu bài viết vào danh sách đọc riêng của bạn và theo dõi tác giả hay chủ đề cho mục cá nhân Theo Trả lời cho bài viết và bình luận của bạn xuất hiện trong Trả lời cho anh.
Tạo cuốn sách hoặc chuỗi sách để kết nối các bài viết đã xuất bản của bạn. Thêm các chương, sắp xếp theo thứ tự, và công khai nội dung khi sẵn sàng. Một tập hợp riêng ẩn danh sách nội dung của nó; các bài viết của nó vẫn được xuất bản riêng lẻ.
Dấu hiệu
∎ được gọi là halmos, sau Paul Halmos, người đã giới thiệu biểu tượng kết thúc chứng minh nó là thứ duy nhất trên trang này mang lại quyền lực, vì vậy nó cố ý khó để có được:
- Chỉ có Lean mới có thể đặt nó.
Truelà bằng chứng, không phải là chứng minh. sorry,native_decide, một cái mớiaxiom,unsafevàdebug.skipKernelTCbị từ chối trước file chạy, vì vậy một kẻ gian lận thậm chí không thể tiêu tốn được thời gian tính toán.- Một chạy được gắn vào chính xác văn bản đã tạo ra nó. Sửa bài và dấu hiệu trở nên cũ thay vì chuyển sang từ mới.
- Nếu một quân bị rơi xuống, anh sẽ "không thể chạy", không bao giờ "từ chối". Tình trạng là công khai vì lý do đó.
The Commons
Kiểm tra là rẻ; khám phá thì không. The Commons ai cũng có thể đóng góp vào nó, không ai sở hữu kết quả, và mỗi lần chạy nó đều được tài trợ công khai, bao gồm cả những cái không đi đâu được, thường là những cái thông tin.
Ai điều hành nó?
Halmos là độc lập và nhỏ. Nếu có gì đó sai ở đây, cách nhanh nhất để chứng minh là một khối mà máy chủ có thể chạy. Gọi cho tôi.