Anthropic dùng Claude hoàn thành xác thực máy tính đầu tiên cho Định lý lớn Fermat trong 11 ngày

Chúng tôi xin chia sẻ bản chứng minh hoàn chỉnh đầu tiên của Định lý lớn Fermat (Fermat’s Last Theorem) đã được máy tính kiểm chứng. Claude đã làm việc gần như tự chủ trong 11 ngày để viết bản chứng minh này bằng ngôn ngữ lập trình Lean. Dưới đây, chúng tôi mô tả cách thức thực hiện quá trình hình thức hóa (formalization) và chia sẻ một số suy nghĩ về ý nghĩa của công trình này đối với nghiên cứu toán học. Khoảng năm 1637, Pierre de Fermat đã ghi lại một khẳng định bên lề cuốn Arithmetica của Diophantus, điều sau này trở thành một trong những phỏng đoán toán học nổi tiếng nhất mọi thời đại: không tồn tại các số nguyên dương a, b, c thỏa mãn aⁿ + bⁿ = cⁿ với mọi n > 2. Định lý lớn Fermat (FLT), như cách gọi sau này, đã trở nên vô cùng khó để chứng minh. Bản chứng minh đầu tiên, từ Sir Andrew Wiles vào năm 1995, dài 129 trang và đòi hỏi nhiều tháng làm việc tỉ mỉ để xác minh.

Một thập kỷ sau, nhà khoa học máy tính người Hà Lan Jan Bergstra đã đề xuất việc "hình thức hóa" bản chứng minh của Wiles: chuyển đổi các lập luận toán học sang dạng mà máy tính có thể tự động kiểm tra. Kể từ đó, các nhà toán học đã phát triển những phương pháp cần thiết để mã hóa một bản chứng minh phức tạp như vậy, bao gồm một nỗ lực cộng đồng kéo dài nhiều năm được khởi xướng vào năm 2024 bởi Kevin Buzzard tại Imperial College London nhằm hoàn thiện quá trình hình thức hóa bằng trợ lý chứng minh Lean.

Gần đây, Tianyi Peng, một nhà nghiên cứu tại Anthropic, người có nhóm làm việc tại Đại học Columbia chuyên xây dựng các công cụ cho việc hình thức hóa bằng AI, đã bắt đầu thử nghiệm xem liệu Claude có thể đạt được tiến bộ trong việc hình thức hóa FLT hay không. Kết quả vượt xa mong đợi của anh. Trong 11 ngày, làm việc gần như tự chủ, Claude đã tạo ra bản chứng minh FLT đầu tiên từ đầu đến cuối được máy tính kiểm chứng. Trong quá trình đó, nó đã viết 13 triệu dòng mã Lean và chứng minh 29.500 định lý trung gian.

Chúng tôi đã chia sẻ bản chứng minh thu được với Kevin Buzzard, người đã nhận xét:

Việc tự động hình thức hóa một bản chứng minh phức tạp như FLT là một bước tiến quan trọng hướng tới tương lai nơi toàn bộ toán học có thể được kiểm tra một cách dễ dàng. Khi AI tạo ra ngày càng nhiều bản chứng minh, khả năng hình thức hóa công việc một cách dễ dàng có thể giảm bớt gánh nặng đánh giá các kết quả mới (một quá trình có thể mất nhiều năm). Chúng tôi hy vọng rằng việc tin tưởng vào hệ thống tri thức mà toán học được xây dựng trên đó sẽ trở nên dễ dàng hơn, chứ không phải khó khăn hơn.

Thách thức trong việc xác minh các bản chứng minh toán học

Không giống như các công trình gần đây của AI về giả thuyết Riemann, vốn tạo ra toán học mới, điểm mới ở đây chính là việc xác minh—kiểm tra một bản chứng minh toán học giống như cách người ta kiểm tra một phép tính toán học bằng máy tính cầm tay. Việc chứng minh các định lý toán học đòi hỏi phải lắp ghép các chuỗi logic phức tạp, và nếu một mắt xích bị hỏng, mọi thứ theo sau đó có thể trở nên sai lệch. Việc hiểu một kết quả mới đủ sâu để tự tin vào tính đúng đắn của nó có thể mất nhiều tháng, thậm chí nhiều năm làm việc.

Định lý lớn Fermat là một ví dụ minh họa. Fermat đã viết tuyên bố của định lý vào lề một cuốn sách, kèm theo một ghi chú đầy thách thức:

Trong hơn 350 năm, nhiều thế hệ nhà toán học đã tìm kiếm một bản chứng minh cho FLT, dù là "tuyệt diệu" hay không. Năm 1908, một giải thưởng trị giá 100.000 mác vàng Đức (tương đương 1–2 triệu đô la ngày nay) đã được công bố cho bất kỳ ai có thể đưa ra một bản chứng minh đúng, và chỉ riêng trong năm đầu tiên đã có 621 nỗ lực không thành công.

Vào tháng 6 năm 1993, Wiles đã trình bày cái mà ông tin là bản chứng minh đúng đầu tiên của FLT trong một loạt bài giảng kéo dài ba ngày. Sau hai tháng nỗ lực xác minh chuyên sâu bởi một số nhà toán học, một người phản biện đã đặt cho Wiles một câu hỏi làm lộ ra một lỗ hổng nghiêm trọng. Wiles đã dành một năm để cố gắng khắc phục nó, ban đầu là một mình và sau đó là với cựu sinh viên Richard Taylor. Ông đã ở bên bờ vực từ bỏ dự án khi cuối cùng nhận ra một phương pháp mà ông đã loại bỏ trước đó có thể sửa chữa bản chứng minh.

Wiles đã công bố bản chứng minh đúng đầu tiên của FLT vào tháng 5 năm 1995; nó dựa vào các kỹ thuật toán học hiện đại vốn vượt xa những gì Fermat có thể biết vào năm 1637. Vì một bản chứng minh sơ cấp vẫn chưa được tìm thấy sau nhiều thế kỷ nỗ lực, cộng đồng toán học hiện nay tin rằng "bản chứng minh tuyệt diệu" ban đầu của chính Fermat là không chính xác.

Một cách để kiểm tra tính đúng đắn của bản chứng minh là yêu cầu máy tính thực hiện. Các trợ lý chứng minh như Lean xác minh logic của một bản chứng minh theo thuật toán, chứng minh tính đúng đắn của nó một cách không thể nghi ngờ. Phần khó đối với con người là viết lại bản chứng minh để Lean có thể hiểu được. Trong khi một bản chứng minh viết cho người đọc sẽ bỏ qua nhiều bước hiển nhiên, Lean cần nhìn thấy mọi bước, bất kể nó tầm thường đến đâu. Các bản chứng minh của con người cũng được xây dựng dựa trên nhiều thế kỷ công trình đã xuất bản, trong khi quá trình hình thức hóa bắt đầu từ một phần nhỏ toán học đã được hình thức hóa trước đó.

Đối với FLT, quá trình hình thức hóa dự kiến sẽ mất nhiều năm. Chỉ riêng bản thiết kế mà cộng đồng toán học đang sử dụng để mô tả giai đoạn đầu của dự án đã dài tới 86 trang.

Claude đã hoàn thành bản chứng minh trong 11 ngày, tạo ra các bản chứng minh có thể kiểm chứng bằng máy tính cho 30.300 định lý trong quá trình này (sử dụng 29.500 định lý trong bản chứng minh cuối cùng). Hàng chục tác nhân (agent) Claude đã cộng tác để định nghĩa các khái niệm, chứng minh các định lý trung gian và sử dụng các định lý đó để chứng minh các tuyên bố ngày càng khó hơn. Với 13 triệu dòng mã Lean, bản chứng minh của Claude lớn gấp hơn 5 lần Mathlib, thư viện cộng đồng chính về các bản chứng minh toán học mà định lý này được xây dựng dựa trên đó.

Bản chứng minh của Claude tuân theo một phiên bản đơn giản hóa từ bản chứng minh của Wiles từ Darmon, Diamond và Taylor. Đầu vào toán học từ con người chỉ giới hạn ở các hướng dẫn cấp cao không thường xuyên từ Tianyi: "Jacobian dưới dạng một lược đồ (scheme) có vẻ là ưu tiên cao", "thúc đẩy hoàn thành định lý Mazur sớm". Bạn có thể tìm thấy các đoạn trích về tư duy của Claude tại đây.

Các đoạn trích về tư duy của Claude khi nó nhận ra những gì mình vừa đạt được.

Một số nỗ lực ban đầu của Claude đã thất bại: mặc dù các tác nhân có một số thành công sớm, chúng nhanh chóng mất dấu trạng thái của dự án và ngừng cộng tác hiệu quả. Những nỗ lực thất bại của chúng đóng góp khoảng 7% số dòng mã không phải là mã mẫu (boilerplate) trong bản chứng minh cuối cùng.

Nỗ lực này đã thành công khi chúng tôi chuyển sang sử dụng Prove2Me, một nền tảng cộng tác mở để hình thức hóa toán học do Tianyi Peng và các cộng sự tại Đại học Columbia thiết kế. Prove2Me đã hỗ trợ bằng cách:

Với Prove2Me và hệ thống đa tác nhân dựa trên Claude Code, một nhóm các tác nhân đã hoàn thành bản chứng minh trong chưa đầy hai tuần, tiêu thụ khoảng sáu tỷ token đầu ra từ một mô hình nghiên cứu nội bộ đa năng có khả năng tương đương với Claude Fable 5.1. Bản chứng minh hoàn thiện đã được Lean kiểm tra; nó chỉ sử dụng ba tiên đề tiêu chuẩn của Lean, và một trình so sánh đã xác nhận rằng tuyên bố của định lý khớp với tuyên bố về FLT của chính Mathlib.

Giảm bớt gánh nặng xác minh hình thức

Tốc độ mà chúng tôi có thể tạo ra bản chứng minh này chứng minh rằng hiện nay đã có thể hình thức hóa các mảng lớn của toán học, điều này có thể vừa giúp phát hiện lỗi trong các bản chứng minh toán học thông thường, vừa giảm bớt gánh nặng phản biện các công trình mới. Sau khi xem xét bản chứng minh Lean của Claude, Kevin Buzzard đã nói với chúng tôi:

Hình thức hóa cũng là một yếu tố chính giúp con người có thể tin tưởng vào các kết quả toán học do AI tạo ra. Khi AI và các nhà toán học có sự hỗ trợ của AI tạo ra nhiều bản chứng minh (được cho là) hơn bao giờ hết, việc hình thức hóa có sự hỗ trợ của AI sẽ san sẻ bớt gánh nặng cho các nhà phản biện là con người. Chúng tôi kỳ vọng rằng việc tạo ra một bản chứng minh đã được hình thức hóa đi kèm với bất kỳ tài liệu nào dành cho người đọc sẽ trở nên phổ biến. Mặc dù chúng tôi không nghĩ rằng một bản chứng minh đã hình thức hóa nên thay thế một bài giải thích dễ hiểu cho con người, nhưng đó có thể là cách khả thi duy nhất để cộng đồng toán học bắt kịp với các đóng góp do AI tạo ra.

Việc viết mã Lean cũng dường như giúp Claude chứng minh các kết quả mới. Nhiều kết quả gần đây do Claude thực hiện đã được hình thức hóa song song với các bản chứng minh của chúng, và Claude dường như sử dụng các bản chứng minh một phần này để kiểm tra độc lập các giả thuyết của mình, giống như cách nó viết các mô phỏng số để kiểm tra xem mình có đang đi đúng hướng hay không.

Việc hình thức hóa FLT là một dự án tiêu tốn nhiều token, nhưng đây cũng là bản chứng minh Lean lớn nhất từng được xây dựng. Các nhà nghiên cứu tại Anthropic đã thực hiện một thí nghiệm nhỏ sử dụng ba gói Claude Max cá nhân để hình thức hóa các ứng dụng của Phương pháp vòng Hardy-Littlewood. Cộng tác hoàn toàn thông qua Prove2Me, các tác nhân đã cùng nhau hoàn thành việc hình thức hóa Định lý ba số nguyên tố của Vinogradov chỉ trong ba ngày. Chúng tôi tin rằng với khung hỗ trợ phù hợp, việc hình thức hóa cộng tác các kết quả lớn với các gói đăng ký AI tiêu dùng là hoàn toàn khả thi.

Để đạt được mục tiêu này, Anthropic cũng như các phòng thí nghiệm khác gần đây đã mở rộng hỗ trợ cho các nhà nghiên cứu bên ngoài—bao gồm các nhà toán học làm việc về toán thuần túy và hình thức hóa—với các gói đăng ký miễn phí, giảm giá và tín dụng nghiên cứu. Chúng tôi cũng cung cấp các khoản tài trợ chuyên biệt cho các dự án khoa học lớn hơn, có thể bao gồm việc hình thức hóa các định lý lớn khác hoặc cải thiện Lean hoặc Mathlib.

Với việc AI đang nhanh chóng thay đổi diện mạo của nghiên cứu toán học, các nhà toán học—tại Anthropic và những nơi khác—đang phải vật lộn với ý nghĩa của điều đó đối với công việc của họ. Tuy nhiên, hình thức hóa là một lĩnh vực mà chúng tôi cảm thấy hoàn toàn yên tâm về vai trò của AI. Khi hình thức hóa trở thành một công cụ phổ biến hơn, chúng tôi hy vọng rằng nó sẽ giúp duy trì niềm tin vào hệ thống tri thức toán học chung.

Lời cảm ơn

Nỗ lực hình thức hóa của chúng tôi là một phần nhỏ trong lịch sử lâu dài của định lý Fermat và sự phát triển của toán học hình thức. Bản chứng minh đầy đủ đầu tiên từ Andrew Wiles cùng với Richard Taylor là đỉnh cao của hơn ba trăm năm toán học, tích hợp các ý tưởng từ Gerhard Frey, Jean-Pierre Serre, Ken Ribet, Barry Mazur, Robert Langlands, Jerrold Tunnell, Yutaka Taniyama, Goro Shimura và André Weil, cùng những người khác. Bản chứng minh của Claude tuân theo phần giải thích của Henri Darmon, Fred Diamond và Richard Taylor.

Bản chứng minh của chúng tôi điều chỉnh các phần từ dự án FLT của Imperial College London do Kevin Buzzard dẫn đầu và dự án flt-regular. Lean và Mathlib đều là những công trình tâm huyết và đã nhận được sự đóng góp từ hàng trăm nhà toán học, nhiều người trong số họ làm việc với Lean FRO. Chúng tôi cảm ơn Kevin Buzzard vì đã xem xét bản chứng minh và vì những nhận xét của ông.

Tìm hiểu thêm

Bản chứng minh đầy đủ có sẵn trên GitHub cùng với hướng dẫn chi tiết bằng văn bản về bản chứng minh.

Tài liệu đọc giải thích được đề xuất

Chú thích

Nội dung liên quan

Các nhà nghiên cứu tự động có thể giảm thiểu lỗi căn chỉnh một cách đáng tin cậy

Chúng tôi đã để Claude tự chủ huấn luyện các mô hình nhằm cải thiện hiệu suất của chúng trên một số tiêu chuẩn công cộng đo lường 10 loại lỗi căn chỉnh. Đối với cả 10 loại, Claude đã tìm ra các bản sửa lỗi giúp cải thiện các tiêu chuẩn mục tiêu mà không làm giảm khả năng của mô hình.

Đọc thêm

Cho phép nghiên cứu độc lập về cách mọi người sử dụng Claude

Đầu năm nay, chúng tôi đã thực hiện một chương trình thí điểm cho phép các nhà nghiên cứu bên ngoài truy cập vào dữ liệu sử dụng Claude tổng hợp trong thế giới thực. Ba nhóm nghiên cứu đã thiết kế các nghiên cứu riêng của họ cho Anthropic Insights, công cụ phân tích bảo mật quyền riêng tư của chúng tôi. Trong bài viết này, chúng tôi chia sẻ các kết quả cấp cao từ những nghiên cứu đó và những gì chúng tôi đã học được khi thực hiện chương trình thí điểm này.