ANTHROPIC AI ‘HÌNH THỨC HÓA’ CHỨNG MINH ĐỊNH LÝ CUỐI CÙNG CỦA FERMAT - MỘT CỘT MỐC CHO TOÁN HỌC
Chỉ trong 11 ngày, Claude đã tạo ra bản chứng minh
dài 13 triệu dòng, được máy tính kiểm tra, cho giả thuyết nổi tiếng
đó.
Tác giả: Davide Castelvecchi
 |
| Nhà toán học Andrew Wiles đã hoàn thành chứng minh định lý cuối cùng của Fermat vào năm 1994, hơn 350 năm sau khi Pierre Fermat đề xuất nó. Ảnh: AP Photo/Charles Rex Arbogast/Alamy |
Định lý cuối cùng của Fermat, một trong những kết quả toán học nổi tiếng nhất
trong nửa thế kỷ qua, lần đầu tiên được chuyển thành mã lập trình đã được máy tính kiểm chứng, sử dụng phiên
bản thử nghiệm tiên tiến của chatbot
AI Claude.
Việc một cỗ máy có thể biến công trình của các nhà toán học nhân loại
thành một bản chứng minh đanh thép dài 13 triệu dòng “khiến tôi cực kỳ kinh
ngạc”, Alex Kontorovich, nhà lý thuyết
số tại Đại học Rutgers ở Piscataway, New Jersey, cho biết. Anthropic,
công ty tạo ra Claude, ở San
Francisco, California, đã công bố đột phá này vào ngày 4 tháng 9. Mô hình chỉ cần
11 ngày để hoàn thành một dự án mà người ta dự đoán con người sẽ mất khoảng 10 năm để hoàn thành.
Kết quả này cho thấy trí tuệ nhân tạo (AI) sẽ đóng vai trò ngày càng quan trọng trong việc kiểm tra công trình của các nhà toán học – cũng như trong việc tạo ra các lập luận toán học mới. Với tốc độ tiến bộ hiện tại, việc AI sẽ sớm có khả năng xem xét kỹ lưỡng toàn bộ kho kiến thức toán học không còn là chuyện viển vông nữa, thậm chí chúng có thể phát hiện ra rằng một số kết quả nổi tiếng là sai. “Hai năm trước, đó còn là chuyện viễn tưởng,” Kevin Buzzard, nhà toán học tại Imperial College London, cho biết.
Các nhà toán học kinh ngạc
Các nhà toán học ngày càng kinh ngạc trước tốc độ cải thiện kỹ năng toán học
của AI. Điều này bao gồm khả
năng “hình thức hóa” các chứng
minh của công nghệ này - chuyển đổi các lập luận toán học từ ngôn ngữ tự nhiên thành mã hình thức, có thể được máy tính kiểm chứng, thường là bằng ngôn ngữ lập trình mã nguồn mở được gọi là Lean.
Vào tháng Hai, AI đã đạt một cột mốc khác trong việc hình thức
hóa, khi kiểm chứng công
trình đoạt huy chương Fields của Maryna Viazovska về cách sắp xếp các hình cầu hiệu
quả nhất (trong không gian 8 hoặc 24 chiều). Nhưng Buzzard cho biết độ
phức tạp của công trình nghiên cứu về
định lý cuối cùng của Fermat nằm ở một cấp bậc hoàn toàn khác. Ông nói: “Nó có lẽ phải khó hơn gấp bội”.
Daniel Litt, nhà lý thuyết số tại Đại học Toronto, Canada, có cùng ý
kiến. “Nếu Anthropic có thể hình thức hóa định lý cuối cùng của Fermat, thì có lẽ họ
cũng có thể hình thức hóa bất cứ thứ gì.”
Chứng minh ban đầu của định lý cuối cùng của Fermat, do Andrew Wiles
và Richard Taylor hoàn thành vào năm
1994, là kết quả mang tính bước ngoặt trong toán học thế kỷ XX. Phát biểu tưởng
chừng đơn giản này là: không thể tồn tại bất kỳ số nguyên dương x, y
và z nào sao cho xⁿ + yⁿ = zⁿ, nếu n lớn hơn 2. Nhà
toán học người Pháp Pierre de Fermat đã đưa ra nhận định này vào năm 1637, nhưng không để lại chứng
minh, và nó được biết đến như là định lý cuối cùng “của ông” – mặc dù trong toán học, một phát biểu chỉ
được gọi là định lý sau khi nó đã được chứng minh một cách chặt chẽ là đúng.
(Bản thân việc giải
phương trình cụ thể này – hoặc
biết rằng nó vô nghiệm – không có nhiều ứng dụng thực tiễn, nhưng những kỹ thuật mà Wiles phát triển để giải quyết
vấn đề đã giúp kết nối các lĩnh vực toán học vốn cách xa nhau. Chứng minh này đã mang về cho Wiles giải thưởng Abel, một trong những phần thưởng danh giá nhất trong toán học, vào
năm 2016.)
Việc hình thức hóa một chứng
minh toán học trong Lean đòi hỏi phải 'dạy' trình biên dịch Lean tất cả các
khái niệm sơ bộ và các dữ kiện đã biết trước đó mà bản chứng
minh dựa vào. Để cho phép hình thức hóa các kết quả ngày càng cao
cấp, các nhà toán học đã dày
công tạo ra thư viện mã Lean gọi là Mathlib. Từ năm 2024, Buzzard đã dẫn đầu một dự
án nhắm cụ thể vào định lý cuối
cùng của Fermat, với mục đích
mở rộng Mathlib bằng cách bổ sung hàng ngàn trang kết quả sơ bộ cần thiết để hình thức hóa chứng minh của Wiles và Taylor.
Ông ước tính mình sẽ mất
10 năm để hoàn thành dự án;
trong khi đó, Claude đã tạo ra bản kiểm chứng Lean của riêng nó chỉ trong 11 ngày. Nhưng có một vấn đề. Không giống như Mathlib, code do Claude tạo ra – bao gồm 29.500 'định lý trung gian', theo
Anthropic thì – không thể được
các nhà toán học khác tái sử
dụng ngay lập tức. Việc tích
hợp ít nhất một phần code vào
Mathlib có thể khả thi nhưng
sẽ đòi hỏi một lượng công việc khổng lồ, Buzzard nói, bởi vì thư viện này được
các chuyên gia con người tuyển chọn kỹ lưỡng. Vì vậy, ngay cả khi AI có khả năng kiểm tra hầu
hết mọi chứng minh toán học, cộng đồng có thể phải đối mặt với “một kịch bản ác
mộng”, ông nói, với sự phát triển của nhiều thư viện Lean không tương thích.
‘Chính xác 100%’
Trong trường hợp công trình của Wiles và Taylor, bản chứng minh đã được xem xét kỹ lưỡng và viết lại suốt hàng thập kỷ. Mặc dù dự án của Buzzard đã khắc phục được
một số thiếu sót nhỏ, nhưng chẳng ai thấp thỏm chờ xem toàn bộ chứng
minh rốt cuộc có được Lean kiểm chứng hay không. “Trước đây, tôi chắc 99,9% rằng chứng minh đó đúng,” Buzzard nói. Sau khi công trình của
Anthropic ra mắt, ông nói, “giờ
tôi chắc chắn 100%”.
Nhưng tài liệu toán học đầy rẫy những trường hợp thu hút đông đảo sự chú ý, trong đó các chứng minh dài hàng
trăm trang vẫn đang trong tình trạng lấp lửng, một số thành viên trong cộng đồng khăng
khăng là chúng đúng và những người
khác vẫn hoài nghi. Thông thường, việc xuất bản trên một tạp chí uy tín chỉ là
bước đầu tiên hướng tới sự chấp nhận rộng rãi hơn về tính hợp lệ của một kết quả.
Và nhiều bài báo ít được chú ý có ít độc giả hơn, điều đó càng khiến tình thế của
chúng càng thêm bất trắc. “Tôi
nghĩ ai cũng rõ chuyện hầu hết
các bài báo được xuất bản ngày nay đều có sai sót,” và một số lỗi nghiêm trọng không được phát hiện trong quá trình
bình duyệt, theo Frederick Manners, một nhà toán học tại Đại học California,
San Diego, người có mối quan tâm bên lề liên quan đến AI.
Nhiều nhà toán học hy vọng rằng, sự kết hợp giữa hình thức hóa bằng AI và chứng nhận Lean sẽ đơn giản hóa đáng kể công việc bình duyệt
các công trình nghiên cứu của người khác – điều đặc biệt nhọc nhằn trong lĩnh vực của họ. “Khi số lượng bài báo ngày
càng nhiều, dài hơn và phức tạp hơn, việc bình duyệt tốn thời gian hơn nhưng lại
kém hiệu quả hơn”, Manners nói. “Việc cung cấp cho các nhà toán học một cây đũa
thần có thể nạp một bài báo
trên arXiv và cấp cho họ chứng nhận rằng bài báo đó chính xác, hoặc chỉ ra lỗi,
sẽ vô cùng hữu ích.”
doi: https://doi.org/10.1038/d41586-026-02822-9
Huỳnh Thị Thanh Trúc
dịch
Nguồn: Anthropic AI
‘formalizes’ proof of Fermat’s last theorem — a milestone for mathematics, Nature,
07 September 2026.
