AI chứng minh định lý Fermat trong 11 ngày

Anthropic ngày 4/9 công bố Claude đã hoàn tất bản chứng minh định lý Fermat được máy kiểm tra đầu tiên trong lịch sử, sau 11 ngày chạy gần như tự động. Việc AI chứng minh định lý Fermat ở dạng máy đọc được khép lại một công việc mà giới toán học từng dự tính phải mất nhiều năm. Đây không phải một lời giải mới, mà là bản mã hóa toàn bộ lập luận sang ngôn ngữ Lean để máy tính tự xác nhận từng bước.

Hành trình dẫn tới việc AI chứng minh định lý Fermat bắt nguồn từ khoảng năm 1637, khi Pierre de Fermat ghi bên lề một cuốn sách rằng không tồn tại ba số nguyên dương a, b, c thỏa mãn aⁿ + bⁿ = cⁿ với n lớn hơn 2, kèm chú thích rằng lề sách quá hẹp để chứa lời giải của ông. Phải đến năm 1995, nhà toán học Andrew Wiles mới công bố bản chứng minh đúng đầu tiên, dài 129 trang. Riêng việc kiểm tra bản đó đã ngốn nhiều tháng của một nhóm chuyên gia, và giữa chừng còn lộ ra một lỗ hổng khiến Wiles mất thêm một năm để vá.

Chính chi phí kiểm chứng đó là lý do cộng đồng toán học theo đuổi hướng “hình thức hóa”: dịch chứng minh sang một ngôn ngữ như Lean để trợ lý chứng minh tự kiểm tra logic. Năm 2024, giáo sư Kevin Buzzard tại Đại học Hoàng gia London khởi động một dự án cộng đồng nhiều năm cho riêng bài toán này. Chỉ bản thiết kế mô tả giai đoạn đầu đã dài 86 trang, nên kịch bản AI chứng minh định lý Fermat gọn trong hai tuần nằm ngoài mọi dự đoán của giới chuyên môn.

Thử nghiệm dẫn tới việc AI chứng minh định lý Fermat do Tianyi Peng, nhà nghiên cứu của Anthropic và có nhóm tại Đại học Columbia, khởi xướng nhằm xem Claude tiến được tới đâu. Trong 11 ngày, hàng chục tác tử Claude chạy song song đã viết 13 triệu dòng Lean, chứng minh 30.300 định lý trung gian và dùng 29.500 trong số đó cho bản cuối cùng. Toàn bộ chiến dịch tiêu tốn khoảng sáu tỷ token đầu ra. Bản chứng minh thu được lớn gấp hơn năm lần Mathlib, thư viện toán hình thức hóa lớn nhất của cộng đồng.

Kết quả không đến ngay. Những lần chạy đầu tiên thất bại vì các tác tử nhanh chóng mất dấu trạng thái dự án và ngừng phối hợp hiệu quả; phần việc hỏng đó chỉ đóng góp khoảng 7% số dòng có ý nghĩa trong bản cuối. Nhóm nghiên cứu chỉ thành công khi chuyển sang Prove2Me, nền tảng mã nguồn mở do Peng và cộng sự ở Columbia thiết kế. Prove2Me duy trì một đồ thị có hướng các mệnh đề cần chứng minh, nhờ đó mỗi tác tử biết nên làm gì tiếp theo thay vì phải nhớ toàn bộ bối cảnh. Đây chính là mảnh ghép giúp AI chứng minh định lý Fermat đi trọn quãng đường thay vì dừng ở nửa chừng. Can thiệp của con người gần như chỉ gói trong vài chỉ dẫn ngắn về việc nên ưu tiên nhánh nào.

Buzzard, người được mời rà soát bản AI chứng minh định lý Fermat, gọi đây là một “thành tựu tự động hình thức hóa phi thường” và lưu ý bản chứng minh không dựa trên giả thiết nào ngoài các tiên đề toán học. Bản cuối được Lean kiểm tra, chỉ dùng ba tiên đề chuẩn của ngôn ngữ này, và một công cụ so khớp đã xác nhận phát biểu định lý trùng khớp với phát biểu trong Mathlib.

Vì sao việc AI chứng minh định lý Fermat lại quan trọng với toán học

Giá trị của sự kiện AI chứng minh định lý Fermat nằm ở khâu kiểm chứng chứ không ở nội dung toán học. Một chứng minh dài có thể mất hàng năm để cộng đồng thẩm định, và lịch sử ngành đã có những kết quả sai được chấp nhận trong thời gian dài trước khi bị phát hiện. Nếu việc hình thức hóa trở nên rẻ và nhanh, gánh nặng đó chuyển từ người sang máy.

Sức ép này đang tăng vì chính AI cũng bắt đầu sản xuất kết quả toán học. Khi số bản thảo do mô hình sinh ra nhiều lên, việc kèm theo một chứng minh đã hình thức hóa có thể là cách khả thi duy nhất để giới chuyên môn theo kịp. Anthropic cho biết nhóm nghiên cứu còn làm một thử nghiệm nhỏ chỉ với ba gói thuê bao cá nhân, và các tác tử đã hình thức hóa xong định lý ba số nguyên tố của Vinogradov trong ba ngày. Nói cách khác, quy mô như bài toán Fermat cần hạ tầng lớn, nhưng những bài toán vừa phải đã nằm trong tầm với của cá nhân. Thứ tạo khác biệt trong lần AI chứng minh định lý Fermat này là hạ tầng điều phối, không phải một mô hình đơn lẻ mạnh hơn.

Điều người học AI ở Việt Nam có thể rút ra

Với người đọc trong nước, câu chuyện AI chứng minh định lý Fermat ít liên quan tới toán cao cấp hơn là tới cách vận hành tác tử. Bài học kỹ thuật rõ nhất là các tác tử AI thất bại không phải vì thiếu năng lực suy luận, mà vì mất trí nhớ về trạng thái công việc chung. Thứ cứu dự án là một cấu trúc điều phối bên ngoài mô hình. Đây cũng là nguyên tắc áp dụng được cho mọi quy trình nghiên cứu tự động hay hệ thống nhiều tác tử ở quy mô doanh nghiệp nhỏ.

Điểm thứ hai là chi phí. Sáu tỷ token đầu ra là con số ngoài tầm với của phần lớn nhóm ở Việt Nam, nhưng thử nghiệm Vinogradov cho thấy ngưỡng vào cuộc thấp hơn nhiều khi bài toán được chia nhỏ và có nền tảng cộng tác. Với sinh viên toán hoặc khoa học máy tính muốn thử, Lean và Mathlib đều miễn phí, còn các phòng thí nghiệm lớn đang mở rộng chương trình cấp tín dụng nghiên cứu. Người mới có thể bắt đầu từ hướng dẫn học AI từ A-Z trước khi bước vào mảng chứng minh hình thức.

Cần nói rõ giới hạn: việc AI chứng minh định lý Fermat ở đây là dịch lại một lời giải đã có của con người, không phải phát hiện toán học mới. Bản thân Anthropic cũng nhấn mạnh chứng minh hình thức hóa không thay thế được phần trình bày cho người đọc hiểu. Điều đáng theo dõi trong vài tháng tới là liệu cách làm này có được áp dụng cho những định lý lớn khác đang chờ kiểm chứng hay không.

Nguồn: Anthropic, SiliconANGLE.

Xem thêm: Phân quyền AI agent: 6 nguyên tắc 2026

Đọc thêm: Anthropic sắp có lãi, đón Andrej Karpathy về đội ngũ · ChatGPT dành cho tuổi teen ra mắt tại Mỹ 2026 · Công cụ AI 2026: cách chọn, đánh giá và dùng