Lịch sử toán học: Claude chứng minh thành công Định lý cuối cùng của Fermat sau 11 ngày

Trong một cột mốc quan trọng cho cả trí tuệ nhân tạo và toán học, Anthropic thông báo rằng mô hình Claude của họ đã tạo ra bản chứng minh hoàn chỉnh, được kiểm chứng bằng máy tính — lần đầu tiên — cho Định lý cuối cùng của Fermat (Fermat's Last Theorem - FLT). Thành tựu này được thực hiện gần như tự động trong 11 ngày bằng ngôn ngữ lập trình Lean, tạo ra một trong những bản formalization (hình thức hóa) phức tạp nhất từ trước đến nay.

Kết quả này không chỉ khẳng định năng lực suy luận của AI mà còn mở ra một tương lai nơi toàn bộ toán học có thể được kiểm chứng tự động, giảm tải cho các nhà toán học trong việc đánh giá các kết quả mới — một quá trình trước đây có thể mất nhiều năm.


Thách thức lịch sử của việc kiểm chứng toán học

Vào khoảng năm 1637, Pierre de Fermat đã ghi chú một phỏng đoán bên lề cuốn sách của mình: không tồn tại các số nguyên dương a, b, c thỏa mãn aⁿ + bⁿ = cⁿ với bất kỳ n > 2 nào. Ông tuyên bố đã có một chứng minh tuyệt vời nhưng "lề sách quá hẹp để chứa nó".

Trong hơn 350 năm, các nhà toán học đã cố gắng tìm ra chứng minh. Mãi đến năm 1995, Sir Andrew Wiles mới công bố chứng minh đầu tiên đúng, kéo dài 129 trang, sau nhiều tháng rà soát khắc nghiệt và cả một năm sửa chữa lỗ hổng nghiêm trọng do một nhà phản biện phát hiện. Câu chuyện này cho thấy việc kiểm chứng một chứng minh phức tạp có thể tiêu tốn thời gian và công sức đến mức nào, thậm chí có thể trì hoãn việc công nhận các kết quả khoa học trong nhiều năm.

Claude đã "hình thức hóa" Định lý Fermat như thế nào?

Hình thức hóa (formalization) là quá trình chuyển đổi một chứng minh toán học viết cho con người thành một dạng mà máy tính có thể kiểm chứng logic một cách tự động. Các trợ lý chứng minh như Lean yêu cầu phải thể hiện mọi bước logic, kể cả những bước hiển nhiên nhất, một điều mà chứng minh truyền thống thường bỏ qua.

Khởi đầu, các nỗ lực của Claude gặp thất bại do mất phương hướng và thiếu sự phối hợp giữa các "đại lý" (agent) AI. Tuy nhiên, mọi thứ đã thành công khi nhóm nghiên cứu chuyển sang sử dụng Prove2Me — một nền tảng cộng tác mã nguồn mở do Tianyi Peng (nhà nghiên cứu tại Anthropic, Đại học Columbia) thiết kế. Prove2Me cung cấp một biểu đồ có hướng (DAG) về các định lý, giúp các agent quyết định bước chứng minh tiếp theo, tăng tốc biên dịch và cho phép nhiều agent làm việc song song.

Kết quả đạt được:

• 13 triệu dòng mã Lean được viết — lớn gấp 5 lần thư viện Mathlib (thư viện chứng minh cộng đồng chính).
• 30.300 định lý trung gian được chứng minh, trong đó 29.500 định lý phục vụ trực tiếp cho chứng minh cuối cùng.
• Toàn bộ quá trình tiêu tốn khoảng 6 tỷ token đầu ra từ một mô hình nghiên cứu nội bộ.
• Bản chứng minh tuân theo một phiên bản giản lược của chứng minh Wiles từ Darmon, Diamond và Taylor, dựa trên các công trình của nhiều nhà toán học nổi tiếng như Frey, Serre, Langlands...

Ý nghĩa lớn cho toán học và các lĩnh vực khác

Thành tựu này được Kevin Buzzard, giáo sư tại Imperial College London và là người đứng đầu dự án formalization FLT từ năm 2024, đánh giá là "phi thường". Ông nhấn mạnh rằng thời điểm này có thể dẫn đến việc tự động hóa formalization cho toàn bộ văn thư toán học hiện đại, giúp phát hiện sai sót trong các chứng minh lâu đời và giảm tải đáng kể công việc phản biện (refereeing).

Với sự bùng nổ của toán học do AI tạo ra, khả năng formalization nhanh chóng sẽ trở thành một "công cụ kiểm định" thiết yếu. Các nhà nghiên cứu có thể tin tưởng vào các kết quả do AI sinh ra mà không cần phải kiểm tra thủ công từng bước. Theo các nhà nghiên cứu tại Anthropic, văn bản toán học có thể sẽ được xuất bản song song với bản formalization, nhằm đảm bảo tính đúng đắn tuyệt đối.

Hướng tới tương lai: Tiếp cận đại chúng với các gói AI tiêu dùng

Một thí nghiệm nhỏ khác của Anthropic cho thấy ngay cả các gói đăng ký cá nhân (như Claude Max) cũng có thể thực hiện formalization phức tạp: ba tài khoản này đã cùng nhau chứng minh xong Định lý ba số nguyên tố của Vinogradov chỉ trong ba ngày. Điều này mở ra hy vọng rằng sự hợp tác giữa con người và AI trong toán học sẽ ngày càng trở nên dễ tiếp cận hơn.

Bộ chứng minh đầy đủ đã được công bố công khai trên GitHub cùng với bản giải thích chi tiết, cho phép cộng đồng toán học và công nghệ trên toàn thế giới — trong đó có các nhà nghiên cứu và kỹ sư phần mềm tại Việt Nam — có thể tự nghiên cứu và đánh giá.

Đây là một bước đi chứng minh rằng AI không chỉ tạo ra những suy luận mới mà còn củng cố niềm tin vào những thành tựu tri thức của loài người, một nhiệm vụ mà trước đây chỉ có con người với khả năng tư duy bậc cao mới có thể thực hiện.