Claude vừa kiểm chứng bản chứng minh toán học 350 năm tuổi trong 11 ngày

Claude của Anthropic vừa hoàn thành bản chứng minh Định lý lớn Fermat đầu tiên được máy tính kiểm chứng toàn bộ.

Tianyi Peng, nhà nghiên cứu tại Anthropic, muốn xem liệu Claude có thể chuyển bài chứng minh năm 1995 của Sir Andrew Wiles sang Lean — một ngôn ngữ lập trình dùng để kiểm tra logic toán học. Tự chạy là chính trong 11 ngày, Claude đã viết 13 triệu dòng code và chứng minh 29.500 định lý phụ để hoàn thành trọn vẹn bài toán.

Vì sao quan trọng: Giới toán học thường mất nhiều tháng, thậm chí nhiều năm để phản biện một bài chứng minh xem có lỗi ẩn nào không. Việc chuyển tư duy phức tạp của con người thành code cho máy chạy giúp AI xác minh toán khó trong chớp mắt. Nghiên cứu mới nhờ đó cũng đáng tin hơn hẳn.

Nên biết: Đây không phải toán mới — mà là dò lỗi tự động. Claude không tự nghĩ ra cách chứng minh mới. Nó chỉ dịch phiên bản đơn giản hóa từ công trình của Wiles sang Lean nhờ hàng chục AI agent phối hợp với nhau. Con người chỉ can thiệp vài chỗ mang tính định hướng, kiểu như bảo mô hình nên giải tiếp định lý nào.

Fermat từng bảo lề trang sách quá hẹp không đủ ghi bản chứng minh; hóa ra ông chỉ thiếu 13 triệu dòng code.