Anthropic cho biết, Claude đã hoàn thành chứng minh hình thức đầu tiên của Định lý Lớn Fermat. Đây không phải là việc phát hiện lại định lý này, mà là chuyển đổi chứng minh hiện có thành mã logic có thể được máy tính kiểm tra từng dòng. Công ty cho biết, công việc này mất 11 ngày và cuối cùng tạo ra khoảng 13 triệu dòng nội dung.
Ý nghĩa của chứng minh hình thức là chuyển các lập luận toán học thành ngôn ngữ có thể được máy tính kiểm tra. Các chứng minh trong bài báo truyền thống thường đòi hỏi thời gian dài kiểm tra bởi các chuyên gia cùng lĩnh vực; nếu có bất kỳ bước nào bị lỗi, quá trình sửa chữa có thể kéo dài hàng tháng甚至 hàng năm. Định lý lớn của Fermat được nhà toán học người Anh Andrew Wiles chứng minh vào năm 1995, nhưng việc chuyển toàn bộ chứng minh này thành phiên bản có thể kiểm tra bằng máy vẫn được coi là một dự án kỹ thuật cực kỳ phức tạp.
Hoàn thành mục tiêu dự án dài hạn trong 11 ngày
Nhà toán học từ Đại học Imperial London, Kevin Buzzard, đã thúc đẩy dự án liên quan kể từ năm 2024, với mục tiêu tương tự là chuyển đổi chứng minh của Wiles vào trình trợ giúp chứng minh Lean. Theo kế hoạch ban đầu, công việc này đòi hỏi sự hợp tác lâu dài và nguồn vốn đã được bố trí đến năm 2029.
Anthropic cho biết, Claude đã hoàn thành sớm hơn các mục tiêu tương tự trong nhiệm vụ này. Sau khi xem xét, Buzzard cho biết, bằng chứng này có thể được xác lập mà không cần dựa vào các giả định bổ sung, tức là chỉ dựa trên hệ tiên đề cơ bản nhất của toán học để xác minh.
Được thực hiện song song bởi nhiều đại lý
Theo Anthropic, nhóm nghiên cứu của Tianyi Peng tại Đại học Columbia đã cho nhiều đại diện Claude hoạt động song song, mỗi đại diện phụ trách viết định nghĩa và chứng minh các kết luận nhỏ hơn, sau đó dần ghép lại thành các cấu trúc chứng minh lớn hơn. Việc can thiệp của con người ít, chủ yếu chỉ là đưa ra thứ tự ưu tiên theo từng giai đoạn.
Các tiến triển ban đầu không suôn sẻ. Anthropic cho biết, một số đại lý đã từng không thể chia sẻ nội dung đã hoàn thành và lặp lại công việc. Sau đó, nhóm đã sử dụng công cụ có tên Prove2Me để cung cấp danh sách nhiệm vụ và cách tổ chức tệp tin thống nhất cho từng đại lý, đồng thời lưu lại ghi chú bằng ngôn ngữ tự nhiên, giúp chúng tái sử dụng kết quả của nhau.
- Số lượng định lý hỗ trợ vượt quá 30.000
- Tổng lượng tiêu thụ đạt hàng tỷ token
- Cuối cùng, chứng minh khoảng 13 triệu dòng
Chú trọng vào tính xác minh thay vì định lý mới
Sự nhấn mạnh của thành quả lần này không nằm ở việc phát hiện các định lý toán học hoàn toàn mới, mà ở việc chuyển đổi các chứng minh quan trọng đã có thành phiên bản có thể được máy tính kiểm tra từng bước. Khi số lượng bài báo toán học và nội dung do AI tạo ra ngày càng tăng, chi phí kiểm tra thủ công từng bước các chứng minh cũng tăng theo, do đó các công cụ hình thức hóa ngày càng được quan tâm nhiều hơn.
Anthropic cũng cho biết, chứng minh này có quy mô lớn hơn 5 lần so với thư viện chung thường được sử dụng trong cộng đồng toán học Mathlib. Tệp đầy đủ đã được tải lên GitHub, cho phép các nhà nghiên cứu tiếp tục kiểm tra từng dòng cấu trúc và tính chính xác của nó.