Claude được cho là đã chính thức hóa Định lý cuối cùng của Fermat trong Lean chỉ sau 11 ngày như thế nào

Anthropic cho biết Claude đã tạo ra bản chính thức hóa Lean hoàn chỉnh, được máy kiểm tra từ đầu đến cuối, cho Định lý cuối cùng của Fermat (FLT). Điểm cần phân biệt rõ: Claude không tìm ra chứng minh mới cho FLT. Hệ thống đã chuyển một hướng chứng minh hiện đại vốn đã được thiết lập thành một hiện vật phần mềm khổng lồ để Lean có thể kiểm tra cơ học. Theo Anthropic, quá trình này kéo dài 11 ngày với phần lớn công việc do các tác tử tự chủ thực hiện và tạo ra khoảng 13 triệu dòng mã Lean. 215

Claude đã chính thức hóa điều gì?

FLT nói rằng với các số tự nhiên và số mũ từ 3 trở lên, phương trình (a^n+b^n=c^n) không có nghiệm không tầm thường. Trong cách phát biểu của Mathlib — thư viện toán học cho Lean — mọi nghiệm đều phải có (a=0), (b=0) hoặc (c=0). Điều này tương đương với phát biểu quen thuộc rằng không tồn tại nghiệm nguyên dương. 31

Dự án đi theo cách trình bày Darmon–Diamond–Taylor của chiến lược Wiles/Taylor–Wiles, thay vì phát minh một lộ trình toán học mới. Đây là khác biệt then chốt: khi chính thức hóa, không chỉ lập luận chính mà cả định nghĩa, giả thiết, kết quả bổ trợ và những liên kết thường bị lược bỏ trong bài báo toán học đều phải được viết rõ. Dự án FLT tại Imperial College London trước đó cũng mô tả lộ trình của mình là một biến thể hiện đại của chứng minh Wiles/Taylor–Wiles. 511

Vì sao cần tới 13 triệu dòng mã?

Trợ lý chứng minh hình thức không chấp nhận kiểu viết “suy ra bằng một lập luận chuẩn”. Mỗi suy luận phải được diễn đạt sao cho hệ thống có thể kiểm tra kiểu dữ liệu và tính hợp lệ; mỗi kết quả cũng phải dựa trên các phụ thuộc đã được chính thức hóa.

Anthropic báo cáo rằng dự án đã tạo khoảng 30.300 định lý được máy kiểm tra, trong đó khoảng 29.500 định lý xuất hiện trong chuỗi phụ thuộc dẫn đến kết quả cuối. Bản phát triển bao trùm đại số, hình học, giải tích điều hòa và lý thuyết số. 215

Vì vậy, không nên hiểu con số 11 ngày là thay thế cho toàn bộ lịch sử trí tuệ phía sau FLT. Anthropic cũng cho biết hệ thống đã sinh khoảng 6 tỷ token. Khối lượng đó bao gồm nhiều phương án chứng minh, các lượt Lean kiểm tra, sửa lỗi theo phản hồi và công việc kỹ thuật để tổ chức một dự án hình thức hóa dài hạn. 5

Mấu chốt: điều phối nhiều tác tử từ bên ngoài mô hình

Kết quả này không đơn thuần đến từ một mô hình duy trì toàn bộ chứng minh khổng lồ trong ngữ cảnh. Anthropic nói các nỗ lực ban đầu có tiến triển nhưng gặp khó khăn khi duy trì trạng thái chung của dự án. Lần chạy thành công dùng một bộ điều phối dựa trên Prove2Me, nền tảng dành cho việc chính thức hóa toán học theo hướng cộng tác. 529

Ý tưởng tổ chức trung tâm là một đồ thị phụ thuộc có hướng:

• Các nút là định nghĩa, bổ đề hoặc định lý còn thiếu.
• Các cạnh cho biết kết quả nào cần thiết để suy ra kết quả khác ở phía sau.
• Tác tử có thể chọn việc còn mở và hữu ích, chứng minh nó trong Lean, rồi cung cấp kết quả cho tác tử khác tái sử dụng.
• Hệ thống từ đó xây dần từ các thành phần nền tảng lên đến định lý cuối cùng.

Prove2Me mô tả mô hình này là khởi chạy các “nhiệm vụ” chính thức hóa để tác tử đóng góp những chứng minh hình thức có thể tái sử dụng. 29 Trên thực tế, đồ thị biến một nhiệm vụ dài và dễ đổ vỡ thành nhiều bài toán nhỏ có thể kiểm tra, đồng thời lưu giữ trí nhớ dự án bên ngoài một phiên chạy riêng lẻ của mô hình.

“Được máy kiểm tra” thực sự có nghĩa gì?

Anthropic cho biết dự án cuối không có chỗ giữ chỗ sorry — cơ chế Lean dùng để thừa nhận một mệnh đề mà chưa chứng minh — và chỉ dựa trên ba tiên đề chuẩn của Lean. 5

Điều này mạnh hơn rất nhiều so với việc AI viết một chứng minh bằng ngôn ngữ tự nhiên nghe có vẻ thuyết phục. Hạt nhân (kernel) của Lean kiểm tra liệu mọi bước đã mã hóa có tuân theo các quy tắc logic, tiên đề và các phụ thuộc đã nhập hay không. Anthropic cũng nói họ đã kiểm tra để mệnh đề đích khớp với phát biểu FermatLastTheorem đã có trong Mathlib. 531

Tuy nhiên, việc kernel kiểm tra có một ranh giới rõ ràng: nó xác nhận mệnh đề hình thức đã được mã hóa, chứ không tự xác nhận rằng mọi định nghĩa và mệnh đề trung gian đều phản ánh chính xác ý nghĩa toán học không hình thức mà con người muốn nói. Vì thế, khả năng biên dịch độc lập hiện vật được công bố và việc chuyên gia rà soát chuỗi phụ thuộc vẫn là các phép thử thiết yếu.

Vì sao Kevin Buzzard gọi đây là thành tựu đặc biệt?

Theo báo cáo của Anthropic, nhà toán học Kevin Buzzard gọi kết quả này là một “thành tựu chính thức hóa tự động phi thường”. 21 Ý nghĩa không chỉ là tác tử có thể giải những bài Lean đơn lẻ. Điều đáng chú ý là tuyên bố rằng chúng đã lắp ghép được một công trình hình thức nhiều tầng, có thể tái sử dụng, ở quy mô mà trước đây người ta dự đoán sẽ cần nhiều năm lao động phối hợp của con người.

Nếu cách làm này có thể tái lập với chi phí hợp lý, nó có thể hỗ trợ toán học theo một số hướng:

• Kiểm chứng chặt chẽ hơn: hệ thống hình thức có thể phát hiện giả thiết bị thiếu, phép biến đổi không hợp lệ hoặc định nghĩa không khớp mà văn bản thông thường khó bộc lộ.
• Hạ tầng tái sử dụng: một khi bổ đề đã được chính thức hóa, dự án sau có thể nhập lại và dựa vào sự kiểm tra của kernel thay vì dựng lại toàn bộ chi tiết.
• Bổ sung cho bình duyệt: chứng minh có thể kiểm tra bằng máy có thể giảm gánh nặng xác minh các lập luận kỹ thuật dài, trong khi nhà toán học vẫn đánh giá ý nghĩa, mức độ liên quan và chiến lược.

Đây là các lợi ích tiềm năng, không phải sự thay thế tự động cho phán đoán toán học. Một chứng minh hình thức có thể hợp lệ về logic nhưng vẫn đang chứng minh nhầm mệnh đề; đồng thời, chi phí tạo ra một hiện vật 13 triệu dòng vẫn rất lớn.

Cách hiểu đúng về tuyên bố này

Kết quả FLT được công bố là một cột mốc đáng kể cho việc AI hỗ trợ chính thức hóa, bởi mục tiêu là một định lý đã được xác lập và hiện vật cuối được thiết kế để có thể kiểm tra độc lập. Nhưng không nên mô tả đây là việc Claude vừa giải mới Định lý cuối cùng của Fermat.

Cách diễn giải mạnh nhất nhưng chính xác hơn là: Anthropic báo cáo rằng một hệ tác tử được điều phối đã chuyển một chứng minh lớn đã biết thành bản phát triển Lean ở quy mô chưa từng có, bằng cách chia việc theo đồ thị phụ thuộc và dùng kiểm chứng hình thức làm phản hồi. 21529

Các câu hỏi tiếp theo mang tính thực tế: giới nghiên cứu bên ngoài có tái lập được bản dựng hay không, có thể kiểm tra ý nghĩa toán học của quá trình hình thức hóa hay không, các thành phần có dùng lại được không, và kết quả tương tự có lặp lại với những bài toán hiện đại khác không. Những phép thử đó sẽ cho biết đây là một kỳ công kỹ thuật đơn lẻ hay một thay đổi bền vững trong cách xây dựng và kiểm tra chứng minh toán học.