AI không chỉ hỗ trợ trong việc chứng minh một định lý toán học nổi tiếng. Nó đã giúp biến chứng minh đó thành khả năng kiểm tra bởi máy tính. Anthropic cho biết @claudeai đã hoạt động chủ yếu tự chủ trong 11 ngày để tạo ra bản hình thức hóa hoàn chỉnh đầu tiên của Định lý Lớn Fermat trong Lean. 13 triệu dòng chứng minh hình thức. 29.500 định lý trung gian được sử dụng trong kết quả cuối cùng. Sự khác biệt này rất quan trọng. Andrew Wiles đã chứng minh Định lý Lớn Fermat cách đây nhiều thập kỷ rồi. Đột phá ở đây là chuyển đổi một khối lượng toán học con người cực kỳ phức tạp thành thứ mà máy tính có thể xác minh toàn bộ từ đầu đến cuối. Và tôi nghĩ điều này chỉ ra một trong những vai trò quan trọng nhất mà AI có thể đóng trong khoa học. Không phải thay thế nhà khoa học. Mà là giảm thiểu nút thắt trong việc xác minh. Khi AI tạo ra ngày càng nhiều toán học, mã nguồn và lập luận khoa học, việc đưa ra câu trả lời sẽ trở nên rẻ hơn. Việc chứng minh rằng những câu trả lời đó thực sự chính xác có thể trở nên quý giá hơn. Biên giới tiếp theo của AI có thể không chỉ là trí thông minh. Mà có thể là trí thông minh có thể xác minh được.