Đưa ra tuyên bố. Nhân quyết định liệu nó có được chứng minh hay không.

Một bảng các mô hình tấn công vấn đề của bạn với văn học, SageMath, PARI/GP và một giải SMT, sau đó chính thức hóa kết quả trong Lean 4 so với Mathlib. Nhân của Lean hoặc chấp nhận chứng minh hoặc nó không, và không có số lượng văn xuôi tự tin thay đổi điều đó. Khi nó thất bại bạn sẽ có mục tiêu chính xác còn lại, thường là nơi mà tranh luận không chính thức là tay- lắc.

Mục tiêu
Hãy cụ thể về nghĩa của việc làm. "Chính xác X có đúng không, và chứng minh nó" hơn là "Kể tôi nghe về X".
Đường đi phải rõ ràng.
Cầu xin chứng minh về mức độ giải thưởng và nó sẽ nói rõ cho anh biết khi nào ban giám khảo không đạt được mục tiêu, thay vì tuyên bố chiến thắng.
Bảng điều khiển
Nhiều chỗ ngồi hơn có nghĩa là nhiều góc, và nhiều chi phí hơn mỗi vòng.
Thẩm phán.
Điều chỉnh các tiêu chuẩn và kiểm tra lại mọi bằng chứng, đáng giá như mô hình mạnh nhất của anh.
Vòng tròn
Giới hạn chi tiêu
Đánh vào nó sẽ ngừng match, không mất gì cả.
Tính hiển thị
Đăng ký để bắt đầu một match
Tài khoản mới sẽ được tín dụng ban đầu, đủ cho match thật.
Một người chơi không thể thuyết phục được

Lean 4 với Mathlib kiểm tra kiểu của câu cuối cùng, và một chứng minh dựa trên sorry, native_decide hoặc một tiên đề mới sẽ bị từ chối thay vì được tính. Bên cạnh nó: SageMath, PARI/GP, Z3, CVC5 và OEIS, vì vậy một cấu trúc có thể được tính toán và xác định trước khi ai đó cố gắng chứng minh bất cứ điều gì về nó.

Một chứng cứ thất bại là một phát hiện.

Khi chính thức hóa thất bại, mục tiêu Lean không thể gần được chuyển cho bất kỳ vị trí nào có vị trí tốt nhất để tấn công nó: chỉ mục tiêu đó, không phải toàn bộ lịch sử. Một chứng minh bị từ chối đặt tên khoảng cách chính xác, hơn hầu hết các tranh luận không chính thức từng làm.

Không có gì được chứng minh hai lần.

Mỗi câu lệnh mà bảng điều khiển thiết lập sẽ được ghi trong một bộ ghi chung với chứng minh của nó, vì vậy nó không bao giờ được suy ra lại và các điểm chết không bao giờ được thử lại. Các vấn đề dài sẽ tạm dừng và tiếp tục mà không mất công việc: đóng thẻ và quay lại ngày mai.