Khoảng Theorem.chat.
Theorem.chat lấy một tuyên bố toán học và cố gắng giải quyết nó. Bạn nói ra tuyên bố, và tiêu chuẩn nó phải đáp ứng. Một bảng các mô hình AI — bao nhiêu bạn muốn, từ bất kỳ nhà cung cấp nào bạn muốn — tấn công nó, và một mô hình khác nữa là trọng tài. Sau đó, lập luận được chính thức hóa trong Lean 4 đối với Mathlib, và nhân Lean quyết định liệu nó có được chứng minh hay không. Bước cuối cùng là sản phẩm.
Tại sao là hạt nhân, chứ không phải một mô hình khác
Hãy hỏi một mô hình một câu hỏi khó và bạn sẽ nhận được một câu trả lời dễ hiểu về việc nó đúng hay không. Hỏi nhiều và họ thường đồng ý, cảm giác như là sự xác nhận và không phải: các mô hình chia sẻ dữ liệu huấn luyện và điểm mù chung. Một mô hình thứ hai kiểm tra mô hình đầu tiên vẫn là cùng một loại phán xét, và nó có thể được nói xung quanh. Nhân Lean không thể. Nó hoặc là lấy ra tuyên bố từ các tiên đề và Mathlib, hoặc là không, và sự tin tưởng không có ảnh hưởng đến kết quả.
Các cách thông thường để giả mạo một chứng minh chính thức được kiểm tra và từ chối. Một chứng minh để lại một lỗ hổng với sorry, một chứng minh mà kêu gọi native_decide để làm hạt nhân thực hiện một phép tính trên niềm tin, hoặc một chứng minh mà lặng lẽ giới thiệu một tiên đề mới, được phát hiện và từ chối thay vì được tính là thành công.
Điều mà bảng điều khiển thực sự có thể làm
Đánh giá là phần rẻ nhất. Bảng làm việc với văn học — arXiv, OpenAlex, Crossref — vì vậy một kết quả đã biết được trích dẫn thay vì tái tạo lại một cách tồi tệ. Nó có SageMath và PARI/GP cho tính toán, Z3 và CVC5 cho giải SMT, OEIS tìm kiếm để xác định một chuỗi nó đã xây dựng, và một môi trường Python sandbox không truy cập mạng. Một giả thiết có thể được kiểm tra với mười ngàn trường hợp trước khi ai đó dành một vòng cố gắng chứng minh nó, và một ví dụ ngược lại kết thúc cuộc thảo luận ngay lập tức.
Bằng chứng, không phải lời nói.
Một match không được đánh giá về chất lượng của đối chứng. Đề nghị được phân chia thành các tiêu chuẩn chấp nhận, và một tiêu chuẩn chỉ được giải quyết khi một thứ gì đó đằng sau nó có thể được kiểm tra lại bởi một bên thứ ba: một nguồn với đoạn liên quan được trích dẫn, hoặc mã thực sự được thực hiện với kết quả thực sự của nó. Người phán quyết kiểm tra lại bằng chứng đó trước khi phán quyết, và nó không thể tuyên bố match hoàn thành trong khi một tiêu chuẩn vẫn còn mở.
Anh đã đặt ra tiêu chuẩn
Tiêu chuẩn là của bạn để chọn, và trọng tài giữ nó theo nghĩa đen. Hỏi về những gì một chuyên gia cẩn thận sẽ chấp nhận và bạn sẽ nhận được nó. Hỏi về một tranh luận suy luận hoàn chỉnh với mỗi giả định được nêu ra và bạn sẽ bị xét xử theo đó thay vì. Hỏi về mức giá mà một đề nghị giải thưởng sẽ phải đối mặt, và kết quả trung thực thường là một tài liệu chính xác về nơi ban giám khảo đã thất bại — giá trị hơn một tuyên bố tự tin mà bạn sẽ phải tự kiểm tra.
Để nói rõ hơn: đây không phải là một cỗ máy giải quyết các vấn đề mở. Đây là một cỗ máy từ chối cho phép một đối số được giải quyết khi nó không được giải quyết, và nó sẽ nói cho bạn biết chính xác bước nào đã thất bại.
Một sự chính thức hóa thất bại là kết quả hữu ích
Khi Lean không đóng chứng minh, bạn sẽ có mục tiêu chính xác còn lại. Trong thực tế, đó hầu như luôn luôn là điểm mà tranh luận không chính thức đã được kéo tay — bước mà mọi người đọc phiên bản văn xuôi sẽ gật đầu qua. Mục tiêu đó sau đó được chuyển đến bất kỳ chỗ nào có vị trí tốt nhất để tấn công nó, cùng với những gì đã được thử nghiệm, và không có gì khác. Các mô hình thrash khi chúng bị kẹt, tái diễn bản thân với toàn bộ chi phí; trải qua một câu hỏi cụ thể thay vì thường mở khóa cho một phần nhỏ của token.
Long work survives
Mỗi câu lệnh mà bảng thiết lập đi vào một bộ nhớ chia sẻ với chứng minh của nó, vì vậy kết quả được viết một lần và không bao giờ tái tạo, và các điểm chết được ghi lại để không ai đi lại vào chúng. Matches chạy bên máy chủ và tạm dừng sạch sẽ - trên ngân sách, trên một nhà cung cấp bị gián đoạn, hoặc vì bạn đóng tab - và tiếp tục chính xác nơi họ đã ngừng.
Đây không phải là cái gì
Định lý là một từ suy luận. Trang này được xây dựng cho toán học, logic, khoa học máy tính lý thuyết, vật lý lý thuyết và lý thuyết kinh tế — các lĩnh vực mà một tuyên bố được giải quyết bằng chứng minh. Các câu hỏi thực nghiệm trong sinh học, y học, hóa học hoặc khoa học xã hội không tạo ra định lý, chúng tạo ra kết quả, và không có số lượng chính thức hóa nào sẽ quyết định chúng. Trang chị em referee.chat của chúng tôi chạy cùng một quá trình panel- và- giám khảo mà không có bước Lean, cho chính xác những câu hỏi đó.