Claude hình thức hóa Định lý cuối Fermat trong 11 ngày, không phải chứng minh mới
Ngày 04/09/2026, Anthropic công bố Claude đã hoàn thành bản hình thức hóa Định lý cuối Fermat bằng Lean sau 11 ngày làm việc phần lớn tự chủ. công bố nghiên cứu của Anthropic cho biết các tác tử đã tạo khoảng 13 triệu dòng Lean, chứng minh 30.300 định lý trong quá trình thực hiện và dùng 29.500 định lý trong kết quả cuối.
Cùng ngày, bản tin của SiliconANGLE mô tả đây là việc chuyển chứng minh toán học đã có từ năm 1995 sang dạng máy tính có thể kiểm tra. Vì vậy, Claude không giải lại bài toán từng tồn tại hơn 350 năm và cũng không phát hiện một chứng minh toán học mới.
Ba tầng khác nhau trong kết quả của Claude
Tầng thứ nhất là chứng minh toán học dành cho con người. Tuyến lập luận dẫn đến Định lý cuối Fermat được xây dựng từ công trình của Gerhard Frey, Jean-Pierre Serre, Ken Ribet, Andrew Wiles và Richard Taylor; bản hình thức hóa mới đi theo cách trình bày giản lược của Henri Darmon, Fred Diamond và Richard Taylor. Phần đóng góp của Claude không thay thế tuyến toán học này.
Tầng thứ hai là bản hình thức hóa Lean. Một chứng minh thông thường có thể bỏ qua phép biến đổi quen thuộc, dẫn một kết quả đã biết hoặc dựa vào nền tảng chung của người đọc. Với Lean, các đối tượng, giả thiết, định nghĩa và quan hệ phụ thuộc phải được diễn đạt đủ chính xác để phần mềm xử lý.
Tầng thứ ba là khâu kiểm tra. Claude tạo mã và ghép các nghĩa vụ chứng minh, còn kernel của Lean kiểm tra xem từng khai báo có suy ra hợp lệ từ những định nghĩa, tiên đề và kết quả đã được chấp nhận hay không. Đây là khác biệt cốt lõi giữa một mô hình ngôn ngữ tự đánh giá câu trả lời và một artifact được chuyển cho bộ kiểm tra hình thức riêng biệt.
Claude hoàn thành khối lượng công việc đó như thế nào
Nhiệm vụ không được xử lý như một lời nhắc duy nhất yêu cầu mô hình viết toàn bộ chứng minh. Hàng chục tác tử Claude cùng định nghĩa khái niệm, giải các định lý trung gian và dùng kết quả đã hoàn tất để mở đường đến những nghĩa vụ khó hơn. Đầu vào của con người chủ yếu là chỉ dẫn toán học ở mức cao, thay vì sửa thủ công từng dòng.
Thành phần điều phối quan trọng là Prove2Me, một nền tảng cộng tác do nhóm của Tianyi Peng tại Đại học Columbia phát triển. Hệ thống duy trì đồ thị có hướng không chu trình của các phát biểu và quan hệ phụ thuộc, giúp tác tử nhận biết phần nào đã hoàn thành, phần nào đang được xử lý và kết quả nào có thể tái sử dụng. Nó cũng tách phát biểu khỏi tệp chứa chứng minh để giảm chi phí biên dịch lại khi dự án thay đổi.
Quy mô 13 triệu dòng vì thế không nên được hiểu như thước đo cho độ mới của toán học. Mã hình thức thường dài hơn bản trình bày dành cho chuyên gia vì phải triển khai những bước vốn được ngầm hiểu. Con số này phản ánh khối lượng chuyển đổi và kiểm tra mà hệ thống đã thực hiện, không chứng minh rằng Claude tìm ra một con đường toán học hay hơn hoặc ngắn hơn.
Mã Lean đã công khai nhưng có phần kế thừa
kho mã công khai của Anthropic phát hành artifact theo Apache 2.0 và ghi nhận phần mã kế thừa từ dự án FLT của Imperial College London, flt-regular và Mathlib. Hồ sơ phân bổ nguồn gốc liệt kê 106 tệp có vật liệu từ hai dự án FLT cùng 23 tệp tái sử dụng văn bản Mathlib, nên kết quả không phải một cơ sở mã được Claude viết hoàn toàn từ đầu.
Kho mã khai báo định lý cho các số tự nhiên dương và số mũ từ 3 trở lên. Bản dựng dùng Lean 4.33.1 đã kiểm tra 60.475 mô-đun; comparator đối chiếu phát biểu cuối với một phát biểu độc lập chỉ dựa trên Mathlib, còn kernel nanoda chấp nhận 1.052.234 khai báo trong môi trường xuất ra mà không báo lỗi.
Các kiểm tra còn xác nhận chứng minh chỉ phụ thuộc vào ba tiên đề chuẩn được Lean liệt kê, đồng thời không chứa những lối tắt bị cấm như sorry, tiên đề bổ sung hoặc native_decide. Điều này củng cố kết luận rằng chuỗi suy luận hình thức hợp lệ đối với phát biểu đã mã hóa, nhưng không xóa bỏ nhu cầu xem xét nguồn gốc mã và ý nghĩa toán học của từng định nghĩa.
Autoformalization có giá trị gì và dừng ở đâu
Giá trị trực tiếp của kết quả nằm ở tốc độ chuyển một khối lượng toán học rất lớn sang dạng có thể kiểm tra tự động. Nếu quy trình đạt độ tin cậy tương tự ở những dự án khác, nó có thể giảm lao động thủ công khi phát hiện giả thiết bị thiếu, quan hệ phụ thuộc chưa được nêu rõ hoặc bước suy luận chưa đủ chặt trong bản viết dành cho con người.
Tuy nhiên, kernel chỉ kiểm tra điều thực sự được viết bằng ngôn ngữ hình thức. Nó không tự quyết định rằng một định nghĩa có phản ánh đúng khái niệm mà nhà toán học dự định hay không, cũng không hiểu tên tiếng Anh của một định lý trung gian. Dự án dùng comparator để giảm rủi ro phát biểu cuối bị mã hóa sai, nhưng con người vẫn phải đánh giá việc mô hình hóa và diễn giải kết quả.
Một artifact hợp lệ cũng không đương nhiên là một chứng minh dễ đọc. Mã của dự án được tạo để máy kiểm tra, có tên và nhãn mang dấu vết của quy trình tự động, đồng thời phụ thuộc mạnh vào thư viện và mã nguồn mở có trước. Nó có thể là nền tảng kiểm chứng mà không thay thế bản trình bày giải thích các ý tưởng toán học cho chuyên gia.
Điều đã được xác nhận và phần còn bỏ ngỏ
Ở thời điểm công bố, kết quả xác nhận Claude có thể hình thức hóa đầu-cuối một tuyến chứng minh phức tạp đã biết, tạo artifact Lean công khai và vượt qua nhiều lớp kiểm tra được mô tả trong kho mã. Cách diễn đạt chính xác vì thế là Claude hình thức hóa và giúp máy kiểm tra chứng minh, không phải Claude khám phá lời giải mới cho Định lý cuối Fermat.
Điều chưa được thiết lập là khả năng chuyển nguyên vẹn thành công này sang một kết quả toán học mới, nơi tuyến lập luận chưa tồn tại và bản thân nội dung cần được cộng đồng thẩm định. Việc tái dựng độc lập, đánh giá khả năng bảo trì và xem xét chi tiết hàng triệu dòng mã sẽ cho biết artifact này có thể trở thành nền tảng lâu dài hay chủ yếu là một cột mốc về quy mô autoformalization.
Đọc thêm:
Đăng ký bản tin
Nhận tin Web3, AI và tiền mã hóa mới nhất ngay trong hộp thư.