Thoại Viết Hoàng✔
Writer
Claude của Anthropic vừa đạt một cột mốc đáng chú ý trong lĩnh vực toán học khi chỉ mất 11 ngày để hoàn thành việc hình thức hóa Định lý cuối cùng của Fermat bằng Lean, tạo ra một hệ thống chứng minh khổng lồ mà máy tính có thể kiểm tra từng bước về mặt logic. Đứng sau dự án là Tianyi Peng (Peng Tianyi), cựu sinh viên lớp Yao danh tiếng của Đại học Thanh Hoa, sau đó lấy bằng tiến sĩ tại MIT và hiện là trợ lý giáo sư tại Columbia Business School, đồng thời tham gia nghiên cứu tại Anthropic.
Thành tựu này đang gây chú ý lớn, song cần hiểu đúng rằng Claude không phải là AI đầu tiên tìm ra lời giải cho Định lý cuối cùng của Fermat, bởi bài toán đã được nhà toán học người Anh Andrew Wiles chứng minh từ hơn 30 năm trước. Điểm đặc biệt của dự án lần này là Claude đã giúp chuyển một khối lượng toán học cực kỳ phức tạp thành chứng minh hình thức bằng Lean, cho phép máy tính kiểm tra chặt chẽ từng định nghĩa, giả thiết và bước suy luận thay vì chủ yếu dựa vào quá trình đọc, đánh giá của các nhà toán học.
Câu chuyện của Định lý cuối cùng Fermat bắt đầu từ năm 1637, khi nhà toán học Pháp Pierre de Fermat viết bên lề một cuốn sách rằng phương trình xⁿ + yⁿ = zⁿ không có nghiệm nguyên dương khi n > 2, đồng thời tuyên bố ông đã tìm được một chứng minh tuyệt vời nhưng phần lề quá hẹp để viết ra. Phát biểu tưởng như đơn giản này đã thách thức nhiều thế hệ nhà toán học trong hơn 350 năm, cho đến khi Andrew Wiles công bố chứng minh vào năm 1993. Một lỗ hổng sau đó được phát hiện, buộc Wiles cùng Richard Taylor phải tiếp tục hoàn thiện trước khi chứng minh cuối cùng được xuất bản vào năm 1995.
Mặc dù bài toán đã được giải quyết, việc kiểm tra bằng máy tính toàn bộ hệ thống toán học đứng sau chứng minh lại là một thách thức khác. Trong các công trình toán học thông thường, tác giả có thể bỏ qua những bước mà giới chuyên môn coi là hiển nhiên, trong khi một hệ thống chứng minh như Lean yêu cầu gần như mọi mắt xích logic phải được mô tả chính xác bằng ngôn ngữ hình thức. Nếu một bước suy luận không hợp lệ, Lean sẽ không chấp nhận kết quả, vì vậy việc hình thức hóa có thể hiểu đơn giản là biến một chứng minh mà con người đọc và đánh giá thành một chứng minh đủ chặt chẽ để máy tính tự kiểm tra.
Quy mô của Định lý cuối cùng Fermat khiến công việc này đặc biệt khó khăn. Giáo sư Kevin Buzzard tại Imperial College London từng dẫn dắt một dự án cộng đồng nhằm hình thức hóa những phần toán học cần thiết cho định lý và đây được xem là nhiệm vụ có thể kéo dài nhiều năm. Trong dự án mới, Anthropic sử dụng Claude để tăng tốc mạnh quá trình này, với nhiều AI agent cùng đảm nhận các định nghĩa, định lý trung gian và các phần khác nhau của hệ thống chứng minh.
Theo thông tin được công bố, trong khoảng 11 ngày, Claude đã tạo ra khoảng 13 triệu dòng mã Lean, xây dựng hơn 30.000 định lý, trong đó phần lớn được sử dụng trực tiếp hoặc gián tiếp cho chứng minh cuối cùng. Con số khổng lồ này cũng cho thấy Claude không đơn giản nhận câu lệnh “hãy chứng minh Định lý cuối cùng của Fermat” rồi lập tức đưa ra đáp án, mà phải xây dựng một lượng rất lớn kiến thức toán học trung gian trước khi Lean có đủ cơ sở để kiểm tra kết quả cuối cùng.
Quá trình này ban đầu cũng không diễn ra suôn sẻ. Khi hàng chục Claude agent cùng hoạt động, chúng gặp khó khăn trong việc theo dõi công việc của nhau, dẫn tới nhiều kết quả trùng lặp hoặc không thể sử dụng; lượng mã hữu ích còn lại từ những thử nghiệm thất bại ban đầu chỉ chiếm khoảng 7% hệ thống cuối cùng. Bước ngoặt xuất hiện khi nhóm của Tianyi Peng sử dụng Prove2Me, một hệ thống tổ chức bài toán thành mạng lưới các nhiệm vụ và định lý trung gian, nhờ đó nhiều AI agent có thể làm việc song song nhưng vẫn biết kết quả nào đã hoàn thành và kết quả nào cần được chứng minh tiếp theo.
Có thể hình dung Prove2Me giống như hệ thống quản lý một công trình xây dựng rất lớn: thay vì để hàng chục nhóm tự xây theo cách riêng, toàn bộ công trình được chia thành những hạng mục có quan hệ rõ ràng với nhau, trong đó kết quả của nhóm này trở thành nền tảng cho nhóm khác tiếp tục. Con người vẫn giữ vai trò định hướng ở cấp độ cao, đặc biệt khi cần xác định nên ưu tiên cấu trúc hoặc định lý toán học nào, còn phần lớn công việc viết mã Lean và xử lý hàng chục nghìn định lý trung gian được giao cho các Claude agent.
Kết quả cuối cùng đáng chú ý ở chỗ toàn bộ hệ thống chứng minh đã vượt qua quá trình kiểm tra của Lean. Điều này đặc biệt quan trọng đối với AI tạo sinh, bởi Claude vẫn có thể đưa ra thông tin hoặc lập luận sai giống các mô hình ngôn ngữ lớn khác, trong khi Lean không đánh giá dựa trên việc câu trả lời “nghe có vẻ đúng” mà kiểm tra các bước suy luận theo những quy tắc logic hình thức. Vì vậy, giá trị của dự án không chỉ nằm ở việc AI tạo ra hàng triệu dòng mã, mà ở chỗ khối mã đó cuối cùng có thể được một hệ thống kiểm chứng độc lập xác nhận.
Do đó, nói rằng “Claude giải trong 11 ngày bài toán mà nhân loại mất hơn 350 năm” là không chính xác, bởi công lao chứng minh Định lý cuối cùng của Fermat vẫn thuộc về Andrew Wiles. Thành tựu thực sự của Claude là cho thấy AI có thể rút ngắn đáng kể quá trình biến những công trình toán học cực kỳ phức tạp thành chứng minh hình thức mà máy tính có khả năng kiểm tra từng mắt xích, một công việc trước đây có thể cần nhiều năm lao động của các chuyên gia.
Nếu phương pháp này tiếp tục phát triển, ảnh hưởng của nó có thể vượt xa riêng Định lý cuối cùng Fermat. Trong tương lai, một công trình toán học quan trọng có thể đồng thời tồn tại dưới hai dạng: bản trình bày dành cho con người đọc để hiểu ý tưởng và bản chứng minh hình thức để máy tính kiểm tra tính đúng đắn. Khi đó, AI không nhất thiết thay thế các nhà toán học, mà có thể trở thành công cụ giúp họ xây dựng, hình thức hóa và kiểm tra những chứng minh ngày càng phức tạp, giảm đáng kể nguy cơ một sai sót nhỏ bị bỏ qua trong những công trình kéo dài hàng trăm trang.
Thành tựu này đang gây chú ý lớn, song cần hiểu đúng rằng Claude không phải là AI đầu tiên tìm ra lời giải cho Định lý cuối cùng của Fermat, bởi bài toán đã được nhà toán học người Anh Andrew Wiles chứng minh từ hơn 30 năm trước. Điểm đặc biệt của dự án lần này là Claude đã giúp chuyển một khối lượng toán học cực kỳ phức tạp thành chứng minh hình thức bằng Lean, cho phép máy tính kiểm tra chặt chẽ từng định nghĩa, giả thiết và bước suy luận thay vì chủ yếu dựa vào quá trình đọc, đánh giá của các nhà toán học.
Câu chuyện của Định lý cuối cùng Fermat bắt đầu từ năm 1637, khi nhà toán học Pháp Pierre de Fermat viết bên lề một cuốn sách rằng phương trình xⁿ + yⁿ = zⁿ không có nghiệm nguyên dương khi n > 2, đồng thời tuyên bố ông đã tìm được một chứng minh tuyệt vời nhưng phần lề quá hẹp để viết ra. Phát biểu tưởng như đơn giản này đã thách thức nhiều thế hệ nhà toán học trong hơn 350 năm, cho đến khi Andrew Wiles công bố chứng minh vào năm 1993. Một lỗ hổng sau đó được phát hiện, buộc Wiles cùng Richard Taylor phải tiếp tục hoàn thiện trước khi chứng minh cuối cùng được xuất bản vào năm 1995.
Mặc dù bài toán đã được giải quyết, việc kiểm tra bằng máy tính toàn bộ hệ thống toán học đứng sau chứng minh lại là một thách thức khác. Trong các công trình toán học thông thường, tác giả có thể bỏ qua những bước mà giới chuyên môn coi là hiển nhiên, trong khi một hệ thống chứng minh như Lean yêu cầu gần như mọi mắt xích logic phải được mô tả chính xác bằng ngôn ngữ hình thức. Nếu một bước suy luận không hợp lệ, Lean sẽ không chấp nhận kết quả, vì vậy việc hình thức hóa có thể hiểu đơn giản là biến một chứng minh mà con người đọc và đánh giá thành một chứng minh đủ chặt chẽ để máy tính tự kiểm tra.
Quy mô của Định lý cuối cùng Fermat khiến công việc này đặc biệt khó khăn. Giáo sư Kevin Buzzard tại Imperial College London từng dẫn dắt một dự án cộng đồng nhằm hình thức hóa những phần toán học cần thiết cho định lý và đây được xem là nhiệm vụ có thể kéo dài nhiều năm. Trong dự án mới, Anthropic sử dụng Claude để tăng tốc mạnh quá trình này, với nhiều AI agent cùng đảm nhận các định nghĩa, định lý trung gian và các phần khác nhau của hệ thống chứng minh.
Theo thông tin được công bố, trong khoảng 11 ngày, Claude đã tạo ra khoảng 13 triệu dòng mã Lean, xây dựng hơn 30.000 định lý, trong đó phần lớn được sử dụng trực tiếp hoặc gián tiếp cho chứng minh cuối cùng. Con số khổng lồ này cũng cho thấy Claude không đơn giản nhận câu lệnh “hãy chứng minh Định lý cuối cùng của Fermat” rồi lập tức đưa ra đáp án, mà phải xây dựng một lượng rất lớn kiến thức toán học trung gian trước khi Lean có đủ cơ sở để kiểm tra kết quả cuối cùng.
Quá trình này ban đầu cũng không diễn ra suôn sẻ. Khi hàng chục Claude agent cùng hoạt động, chúng gặp khó khăn trong việc theo dõi công việc của nhau, dẫn tới nhiều kết quả trùng lặp hoặc không thể sử dụng; lượng mã hữu ích còn lại từ những thử nghiệm thất bại ban đầu chỉ chiếm khoảng 7% hệ thống cuối cùng. Bước ngoặt xuất hiện khi nhóm của Tianyi Peng sử dụng Prove2Me, một hệ thống tổ chức bài toán thành mạng lưới các nhiệm vụ và định lý trung gian, nhờ đó nhiều AI agent có thể làm việc song song nhưng vẫn biết kết quả nào đã hoàn thành và kết quả nào cần được chứng minh tiếp theo.
Có thể hình dung Prove2Me giống như hệ thống quản lý một công trình xây dựng rất lớn: thay vì để hàng chục nhóm tự xây theo cách riêng, toàn bộ công trình được chia thành những hạng mục có quan hệ rõ ràng với nhau, trong đó kết quả của nhóm này trở thành nền tảng cho nhóm khác tiếp tục. Con người vẫn giữ vai trò định hướng ở cấp độ cao, đặc biệt khi cần xác định nên ưu tiên cấu trúc hoặc định lý toán học nào, còn phần lớn công việc viết mã Lean và xử lý hàng chục nghìn định lý trung gian được giao cho các Claude agent.
Kết quả cuối cùng đáng chú ý ở chỗ toàn bộ hệ thống chứng minh đã vượt qua quá trình kiểm tra của Lean. Điều này đặc biệt quan trọng đối với AI tạo sinh, bởi Claude vẫn có thể đưa ra thông tin hoặc lập luận sai giống các mô hình ngôn ngữ lớn khác, trong khi Lean không đánh giá dựa trên việc câu trả lời “nghe có vẻ đúng” mà kiểm tra các bước suy luận theo những quy tắc logic hình thức. Vì vậy, giá trị của dự án không chỉ nằm ở việc AI tạo ra hàng triệu dòng mã, mà ở chỗ khối mã đó cuối cùng có thể được một hệ thống kiểm chứng độc lập xác nhận.
Do đó, nói rằng “Claude giải trong 11 ngày bài toán mà nhân loại mất hơn 350 năm” là không chính xác, bởi công lao chứng minh Định lý cuối cùng của Fermat vẫn thuộc về Andrew Wiles. Thành tựu thực sự của Claude là cho thấy AI có thể rút ngắn đáng kể quá trình biến những công trình toán học cực kỳ phức tạp thành chứng minh hình thức mà máy tính có khả năng kiểm tra từng mắt xích, một công việc trước đây có thể cần nhiều năm lao động của các chuyên gia.
Nếu phương pháp này tiếp tục phát triển, ảnh hưởng của nó có thể vượt xa riêng Định lý cuối cùng Fermat. Trong tương lai, một công trình toán học quan trọng có thể đồng thời tồn tại dưới hai dạng: bản trình bày dành cho con người đọc để hiểu ý tưởng và bản chứng minh hình thức để máy tính kiểm tra tính đúng đắn. Khi đó, AI không nhất thiết thay thế các nhà toán học, mà có thể trở thành công cụ giúp họ xây dựng, hình thức hóa và kiểm tra những chứng minh ngày càng phức tạp, giảm đáng kể nguy cơ một sai sót nhỏ bị bỏ qua trong những công trình kéo dài hàng trăm trang.
