Anthropic: Claude mất 11 ngày để hoàn thành chứng minh hình thức đầu tiên cho Định lý Fermat

Theo tin từ IT ngày 5 tháng 9, Anthropic thông báo vào ngày 4 tháng 9 (giờ địa phương) rằng mô hình AI Claude của họ, sau 11 ngày vận hành gần như tự chủ, đã hoàn thành chứng minh hình thức (formal proof) đầu tiên từ đầu đến cuối cho Định lý lớn Fermat (FLT) và đã được máy tính kiểm chứng.

Anthropic cho biết, công trình này không phải là việc tái khám phá chứng minh toán học cho Định lý lớn Fermat, mà là chuyển đổi chứng minh toán học hiện có sang dạng mà trợ lý chứng minh Lean có thể xác minh từng bước.

Lưu ý của IT: Lean là một trợ lý chứng minh được sử dụng để viết và xác minh các chứng minh toán học hình thức, có khả năng kiểm tra các bước logic trong chứng minh thông qua máy tính.

Theo giới thiệu, trong quá trình này, Claude đã tạo ra khoảng 13 triệu dòng mã Lean và chứng minh khoảng 30.300 định lý, trong đó khoảng 29.500 định lý trung gian cuối cùng đã được đưa vào chứng minh hoàn chỉnh của Định lý lớn Fermat. Toàn bộ chứng minh đã được Lean kiểm tra thành công, chỉ sử dụng 3 tiên đề tiêu chuẩn của Lean.

Mục tiêu của công trình này là hình thức hóa chứng minh Định lý lớn Fermat do nhà toán học người Anh Andrew Wiles hoàn thành vào năm 1995.

Định lý lớn Fermat chỉ ra rằng, khi số mũ nguyên n lớn hơn 2, không tồn tại các số nguyên dương a, b, c thỏa mãn aⁿ+bⁿ=cⁿ. Chứng minh gốc của Wiles dài tới 129 trang và độ chính xác của nó đã trải qua nhiều tháng kiểm tra thủ công trước khi được công bố.

Khó khăn của việc hình thức hóa toán học nằm ở chỗ, các chứng minh toán học của con người thường lược bỏ một lượng lớn các bước suy luận được coi là hiển nhiên, trong khi Lean yêu cầu phải xác minh rõ ràng từng mắt xích logic.

Ngoài ra, các nhà toán học từ lâu vẫn thường trích dẫn một lượng lớn các kết quả toán học hiện có chưa được hình thức hóa, do đó việc chuyển đổi một chứng minh hoàn chỉnh sang dạng máy tính có thể xác minh thường đòi hỏi đầu tư rất nhiều thời gian. Trước đó, Anthropic dự đoán công việc hình thức hóa Định lý lớn Fermat có thể mất nhiều năm.

Dự án này được khởi xướng bởi nhà nghiên cứu Tianyi Peng của Anthropic. Claude không thực hiện toàn bộ công việc bởi một tác nhân (agent) duy nhất, mà thông qua sự cộng tác của nhiều tác nhân để hoàn thành việc định nghĩa khái niệm, chứng minh định lý trung gian và suy luận các mệnh đề phức tạp hơn. Dự án đã sử dụng nền tảng Prove2Me do Peng và các cộng sự tại Đại học Columbia phát triển, sử dụng đồ thị có hướng không chu trình (DAG) để ghi lại các định lý cần chứng minh cùng mối quan hệ phụ thuộc của chúng, đồng thời hỗ trợ nhiều tác nhân Claude làm việc song song.

Anthropic cho biết, chứng minh cuối cùng tuân theo phiên bản rút gọn của Darmon, Diamond và Taylor đối với chứng minh của Wiles. Đầu vào toán học mà các nhà nghiên cứu con người cung cấp chủ yếu là một số ít các chỉ dẫn cấp cao, chẳng hạn như xác định mức độ ưu tiên của một số đối tượng hoặc định lý toán học, còn quá trình chứng minh cụ thể chủ yếu do Claude thực hiện.

Toàn bộ dự án đã tiêu tốn khoảng 6 tỷ Token đầu ra, sử dụng một mô hình nghiên cứu nội bộ đa năng có hiệu năng tương đương với Claude Fable 5.1. Quy mô của chứng minh cuối cùng được tạo ra lớn gấp hơn 5 lần so với Mathlib, thư viện chứng minh toán học chính hiện nay.

Anthropic đặc biệt nhấn mạnh rằng, trọng tâm của thành quả này không phải là việc AI tự mình đưa ra một chứng minh mới cho Định lý lớn Fermat. Định lý này đã được Wiles chứng minh từ năm 1995, điểm đổi mới của công trình này nằm ở việc sử dụng AI để tự động hóa quy mô lớn quá trình hình thức hóa chứng minh và để Lean thực hiện kiểm chứng kết quả cuối cùng bằng máy tính.

Anthropic tin rằng, nếu các kỹ thuật hình thức hóa tự động tương tự có thể mở rộng sang nhiều kết quả toán học hiện đại hơn, thì có khả năng sẽ giảm bớt chi phí nhân lực trong việc xác minh các chứng minh mới trong nghiên cứu toán học. Công ty cũng cho biết, khi số lượng kết quả toán học do AI tạo ra tăng lên, việc cung cấp đồng thời phiên bản hình thức hóa cho các chứng minh toán học dành cho con người đọc có thể trở thành thông lệ phổ biến trong tương lai.

Chứng minh Lean hoàn chỉnh của dự án này đã được công khai trên GitHub (https://github.com/anthropics/fermats-last-theorem).

Anthropic cũng cho biết, Kevin Buzzard đã xem xét chứng minh này và nhận định rằng thành quả hình thức hóa tự động này cho thấy việc hỗ trợ AI trong việc hình thức hóa các kết quả toán học lớn đã đạt được những tiến bộ quan trọng.

Đọc thêm:

"Anthropic ra mắt Claude Fable 5.1 và Mythos 5.1: Hiệu năng vượt trội thế hệ trước, giảm giá bộ nhớ đệm 75%"

"Mô hình mới chưa công bố 'lập công', Anthropic tuyên bố Claude đạt bước đột phá lớn trong việc giải quyết Giả thuyết Riemann"