Tôi đã vượt qua một ranh giới, và tôi cảm thấy hơi kinh ngạc. Đây là bằng chứng đầu tiên của tôi được tự động hóa hoàn toàn, được tạo ra bởi LLM và tự động chính thức hóa cho một định lý toán học mới. Hãy để tôi thiết lập vấn đề: chúng ta có ba vòng tròn quay với sáu vị trí mỗi cái, tất cả ba cái giao nhau tại tổng cộng sáu điểm. Chứng minh rằng nhóm các chuyển động mà chúng tạo ra là nhóm đối xứng đầy đủ S_{12}. Đây là một vấn đề mà tôi đã nhận thấy ban đầu trong một câu đố tuyệt vời trong trò chơi Machinarium của Amanita Design. Nhiệm vụ này không quá khó, nhưng rõ ràng có hai bằng chứng: 1. Một tìm kiếm brute-force qua các lớp đồng nhất để đại diện cho tất cả các hoán vị (tôi đã làm điều này nhiều năm trước nhưng chưa bao giờ công bố nó). 2. Một bằng chứng được tạo ra bởi LLM (trong trường hợp này được sản xuất khoảng ba tháng trước bởi GPT-5-Pro), hoặc thực sự là hai bằng chứng, cả hai đều sử dụng một cách xuất sắc một định lý của Jordan về các nhóm nguyên thủy (hoặc một biến thể liên quan chặt chẽ hơn mà thậm chí còn trực tiếp hơn). ( Điều tôi thiếu cho đến tối nay là một công cụ để tự động chính thức hóa bằng chứng này. Nhờ @HarmonicMath , tôi đã có quyền truy cập vào phần mềm đáng chú ý của họ, Aristotle. Tóm lại, đây là những gì tôi đã làm: A. Tự động tạo ra bằng chứng với một LLM (và chạy nó nhiều lần để có được một phiên bản cải tiến hơn). B. Cắt giảm bằng chứng xuống còn văn bản toán học cơ bản—định nghĩa, giả thuyết, lemmas, định lý—với các bằng chứng được cung cấp bởi LLM. C. Chạy hệ thống Aristotle qua đêm (thông qua API). Sáng nay tôi nhận được một phiên bản chính thức hóa hoàn toàn trong Lean (khoảng 700 dòng mã). Mã biên dịch, vì vậy tôi bây giờ có một chứng chỉ xác nhận rằng bằng chứng được tạo ra bởi LLM thực sự dẫn đến một giải pháp đúng. Hơn nữa, tôi đã có một bằng chứng khái niệm, tốt hơn so với brute-force của tôi. Tôi dự định đẩy nó xa hơn đến một lớp rộng hơn của các vấn đề đại số như vậy. Đây là một dự án nhỏ, nhưng đối với tôi cá nhân, nó đánh dấu một cột mốc. Tôi bây giờ có các công cụ mà, với sự phối hợp của tôi, có thể thực sự giúp tôi khám phá, chính thức hóa và nghiên cứu các bằng chứng của các định lý toán học. Điều này không phải là điều đơn giản. Câu hỏi: 1. Điều này sẽ mở rộng như thế nào trong tương lai? 2. Cần bao nhiêu đào tạo để thành công trong những nhiệm vụ như vậy?...