Anthropic vừa thông báo rằng mô hình AI Claude của họ—với sự can thiệp tối thiểu từ con người—đã hoàn thành bản chứng minh hình thức (formal proof) trọn vẹn đầu tiên cho Định lý cuối cùng của Fermat chỉ trong vòng mười một ngày. Dự án này, do Tianyi Peng (cựu sinh viên Đại học Thanh Hoa kiêm nhà nghiên cứu) khởi xướng, sử dụng một khung làm việc đa tác nhân (multi-agent framework) xây dựng trên nền tảng hỗ trợ chứng minh Lean để chuyển đổi chứng minh toán học năm 1995 của Andrew Wiles và Richard Taylor thành mã máy có thể kiểm chứng được. Quá trình hình thức hóa này đòi hỏi việc tạo ra khoảng 13 triệu dòng mã Lean và chứng minh hơn 30.000 bổ đề trung gian, trong đó có khoảng 29.500 bổ đề cấu thành nên lập luận cuối cùng. Được thực hiện bởi hàng chục tác nhân Claude hoạt động đồng thời, quy trình làm việc ban đầu gặp khó khăn trong việc quản lý trạng thái và theo dõi các sự phụ thuộc (dependency). Nhóm nghiên cứu đã giải quyết vấn đề này bằng cách triển khai Prove2Me—một nền tảng cộng tác chuyên dụng giúp tách biệt các phát biểu định lý khỏi phần chứng minh và duy trì một đồ thị phụ thuộc động. Kiến trúc này cho phép tạo chứng minh song song trong khi vẫn bảo toàn tính toàn vẹn logic, giúp hệ thống xử lý được các thành phần phức tạp của lý thuyết số như đường cong Frey, nâng cấp tính mô-đun (modularity lifting), hạ cấp độ (level lowering) và sự tương ứng R=T.

Quy trình kiểm chứng được thực hiện vô cùng nghiêm ngặt. Chứng minh cuối cùng chỉ dựa vào ba tiên đề logic nền tảng trong Lean, hoàn toàn không sử dụng các giả định chưa được chứng minh. Để đảm bảo độ chính xác, Anthropic đã triển khai một công cụ so sánh nhằm đối chiếu mệnh đề cuối cùng với các tiêu chuẩn của Mathlib, đồng thời để toàn bộ môi trường trải qua quá trình kiểm chứng độc lập bởi một bộ kiểm chứng cốt lõi viết bằng ngôn ngữ Rust mang tên nanoda. Quá trình kiểm tra độc lập này đã chấp nhận hơn 1,05 triệu khai báo, qua đó xác nhận tính nhất quán logic của quá trình suy luận. Mặc dù đạt được thành công về mặt tính toán, dự án cũng bộc lộ những thách thức kỹ thuật đáng kể. Cơ sở mã được tạo ra lớn gấp năm lần kích thước hiện tại của Mathlib; nguyên nhân chủ yếu là do các chứng minh do máy tạo ra thường ưu tiên khả năng kiểm chứng hơn là sự súc tích hay khả năng đọc hiểu của con người. Sẽ cần thực hiện tái cấu trúc thủ công trên quy mô lớn để tối ưu hóa mã nguồn, chuẩn hóa các định nghĩa và tách xuất các mô-đun toán học có thể tái sử dụng.

Sáng kiến ​​này tiêu tốn khoảng 6 tỷ token đầu ra và cần tới 153 gigabyte bộ nhớ ở mức cao nhất trong quá trình xây dựng, bên cạnh các quy trình kiểm chứng chuyên sâu. Mặc dù Anthropic chưa công bố tổng chi phí tài chính hay so sánh hiệu quả với quy trình hình thức hóa do con người thực hiện, nhưng thử nghiệm này đã thiết lập một chuẩn mực mới cho lĩnh vực kỹ thuật toán học dựa trên AI. Nó chứng minh rằng các chứng minh quy mô lớn có lịch sử hàng thế kỷ có thể được phân tách một cách hệ thống, xử lý song song và kiểm chứng bằng máy tính, qua đó cung cấp một mô hình có khả năng mở rộng cho các nghiên cứu có sự hỗ trợ của AI trong tương lai. Tuy nhiên, việc thu hẹp khoảng cách giữa các bước suy luận có thể kiểm chứng bằng máy và toán học mà con người có thể hiểu được vẫn là một lĩnh vực nghiên cứu tiên phong đầy sôi động; điều này nhấn mạnh rằng tính đúng đắn hình thức và tính hữu dụng trong toán học hiện là những mục tiêu kỹ thuật tách biệt.

Theo Trending Stories https://hyper.ai/en/stories/53db6eac5bafd06806ceda4f0e2b69a9