Anthropic vừa công bố Claude đã giúp hình thức hóa toàn bộ chứng minh Định lý cuối cùng của Fermat bằng Lean, một hệ thống có thể kiểm tra từng bước logic của chứng minh toán học.
Điều quan trọng là: Claude không phải là AI đầu tiên giải được Định lý Fermat. Bài toán này đã được Andrew Wiles chứng minh từ thập niên 1990. Thành tựu mới ở đây là Claude đã chuyển một chứng minh toán học cực kỳ phức tạp thành dạng mà máy tính có thể kiểm tra chặt chẽ.
Có thể hiểu đơn giản như thế này: nhà toán học viết chứng minh cho con người đọc, trong đó nhiều bước có thể được rút gọn bằng những câu như “suy ra dễ dàng”. Nhưng máy tính không chấp nhận cách viết đó. Mọi bước phải được diễn đạt chính xác. Claude đã tham gia tạo ra một hệ thống chứng minh rất lớn, với hàng triệu dòng mã Lean và hàng chục nghìn định lý trung gian.
Điểm làm kết quả này đáng tin hơn một thông báo quảng cáo thông thường là Anthropic đã công khai mã nguồn. Người khác có thể tải về, dùng Lean để kiểm tra và xem chứng minh có thực sự hợp lệ hay không. Ngoài ra, kết quả còn được các chuyên gia về formal mathematics xem xét và được Nature đưa tin.
Tuy nhiên, cũng cần đọc thông tin này một cách tỉnh táo. Claude không tự nghĩ ra một chứng minh hoàn toàn mới. Hệ thống dựa trên các thành tựu toán học đã có, các tài liệu giải thích chứng minh của Wiles và nhiều thư viện toán học được xây dựng trước đó. Đây cũng không phải chỉ một chatbot ngồi “suy nghĩ 11 ngày”, mà là một hệ thống gồm nhiều AI agent, công cụ quản lý nhiệm vụ và phần mềm kiểm chứng.
Vì vậy, tiêu đề “AI giải được bài toán Fermat trong 11 ngày” là khá gây hiểu nhầm.
Cách nói chính xác hơn là:
Claude đã giúp tạo ra một phiên bản chứng minh Fermat mà máy tính có thể kiểm tra từ đầu đến cuối.
Điều đáng chú ý nhất của nghiên cứu này không nằm ở Fermat, mà ở một hướng phát triển lớn hơn của AI.
Thông thường, AI có thể tạo ra câu trả lời rất thuyết phục nhưng vẫn sai. Trong toán học hình thức, AI không thể chỉ “nói nghe có vẻ đúng”. Nếu một bước sai, hệ thống kiểm chứng sẽ từ chối.
Mô hình mới có thể hình dung như sau:
AI tạo lời giải → máy kiểm tra → phát hiện lỗi → AI sửa → kiểm tra lại.
Nếu cách làm này được mở rộng sang lập trình, thiết kế chip, mật mã hay nghiên cứu khoa học, AI có thể trở nên đáng tin hơn rất nhiều so với chatbot hiện nay.
Về chất lượng nguồn, bài của Anthropic có độ tin cậy khá cao đối với kết quả kỹ thuật cốt lõi vì mã nguồn và chứng minh được công khai để kiểm tra. Tuy nhiên, đây vẫn là công bố của chính công ty tạo ra Claude, chưa phải một bài báo khoa học đã qua phản biện đầy đủ. Các thông tin như “11 ngày” hay mức độ Claude thực sự hoạt động tự chủ vẫn chủ yếu dựa trên mô tả của Anthropic.
Vì vậy, kết luận hợp lý nhất không phải là:
“AI đã vượt qua Andrew Wiles.”
Mà là:
AI đang bắt đầu có khả năng biến những chứng minh toán học cực kỳ phức tạp thành các cấu trúc mà máy tính có thể kiểm tra từng bước.
Đây có thể là một bước tiến quan trọng hướng tới một thế hệ AI không chỉ tạo ra câu trả lời, mà còn tạo ra những kết quả có thể được kiểm chứng.
Trần Ngọc Minh 