Cựu sinh viên lớp Diêu (Yao Class) dẫn dắt: Claude lần đầu tiên chứng minh thành công Định lý lớn Fermat

< img id="wx_img" src="https://www.qbitai.com/wp-content/uploads/imgs/qbitai-logo-1.png" width="400" height="400">

05-09-2026 09:17:56 Nguồn: QbitAI

Cuối cùng đã được cứu nhờ Harness

Mengyao đưa tin từ trụ sở QbitAI

QbitAI | Kênh chính thức QbitAI

Nhân loại đã loay hoay với Định lý lớn Fermat suốt ba thế kỷ rưỡi, vậy mà Claude chỉ mất 11 ngày!?

Vừa mới đây, Anthropic thông báo rằng Claude đã hoàn thành chứng minh đầu tiên từ đầu đến cuối cho Định lý lớn Fermat, một chứng minh có thể được máy tính kiểm tra toàn diện.

Khoảng 13 triệu dòng mã Lean, hơn 30.000 định lý trung gian, và chứng minh cuối cùng sử dụng khoảng 29.500 trong số đó.

Quy mô toàn bộ dự án này đã vượt gấp 5 lần thư viện toán học cốt lõi Mathlib của Lean.

Lần này, Claude không tìm ra một chứng minh hoàn toàn mới cho Định lý lớn Fermat.

Điều mà nó hoàn thành là một công việc khác có khối lượng "đáng kinh ngạc" không kém:

Chuyển đổi hoàn toàn một chứng minh mà các nhà toán học có thể hiểu được thành một chứng minh hình thức mà máy tính có thể kiểm tra từng dòng một, không hề có những chỗ "hiển nhiên là vậy".

Và việc này, giới toán học vốn dĩ đã chuẩn bị tinh thần cho một dự án kéo dài nhiều năm trời????

Hơn 350 năm lịch sử toán học đã được Claude nén vào 13 triệu dòng mã Lean

Trước tiên, hãy nói nhanh về Định lý lớn Fermat là gì.

Định lý này chỉ ra rằng, với mọi số nguyên n > 2, không tồn tại các số nguyên dương a, b, c sao cho: aⁿ+bⁿ=cⁿ.

Mệnh đề này trông có vẻ cực kỳ đơn giản, nhưng độ khó thì cao đến mức vô lý!!

Kể từ khi Fermat để lại mệnh đề này vào thế kỷ 17, các thế hệ nhà toán học như Euler, Legendre, Kummer... đã không ngừng nỗ lực tiến về phía trước, nhưng vẫn không thể đưa ra được một chứng minh hoàn chỉnh.

Mãi đến năm 1993, nhà toán học người Anh Andrew Wiles mới lần đầu tiên công khai tuyên bố đã chứng minh được Định lý lớn Fermat.

Sau đó, quá trình thẩm định đã phát hiện ra một lỗ hổng then chốt trong chứng minh này.

Wiles đã mất thêm khoảng một năm cùng với Richard Taylor để sửa chữa, và cuối cùng hoàn thành chứng minh vào năm 1994. Đến đây, mệnh đề đã làm đau đầu giới toán học suốt hơn 350 năm mới chính thức được chinh phục...

Nhưng! Giới toán học sau đó lại tự đào cho mình một cái hố mang tính kỹ thuật hơn—

Liệu có thể để máy tính xác nhận 100% rằng chứng minh này là đúng hay không?

Đây chính là cái gọi là "hình thức hóa" (formalization).

Hiểu đơn giản, các bài báo toán học thông thường được viết cho các nhà toán học đọc, não người khi nhìn thấy nhiều bước có thể nói ngay: "Ừ, chỗ này hiển nhiên là đúng rồi~"

Nhưng Lean, một hệ thống trợ lý chứng minh chuyên kiểm tra các chứng minh toán học, thì không chấp nhận kiểu đó...

Chúng ta có thể coi Lean như một "trình biên dịch siêu nghiêm ngặt" trong thế giới toán học—

Các nhà toán học hoặc AI chịu trách nhiệm viết các định lý, định nghĩa và chứng minh từng bước một thành dạng mà Lean có thể hiểu được; còn Lean chịu trách nhiệm kiểm tra xem liệu mỗi bước suy luận có được rút ra một cách hợp lệ từ các tiên đề và định lý trước đó hay không.

Đây cũng là lý do tại sao việc hình thức hóa một chứng minh toán học hiện đại quy mô lớn thường có khối lượng công việc khổng lồ đến kinh ngạc!!

Vào những năm 2000, các nhà khoa học máy tính đã từng đưa ra ý tưởng hình thức hóa chứng minh của Wiles.

Đến năm 2024, Kevin Buzzard và các cộng sự tại Đại học Imperial College London mới chính thức khởi động một dự án cộng đồng kéo dài nhiều năm, chuẩn bị sử dụng Lean để hoàn thành việc hình thức hóa Định lý lớn Fermat. Chỉ riêng bản kế hoạch kỹ thuật cho giai đoạn đầu của dự án đã dài tới 86 trang.

Kết quả là sau khi Claude xuất hiện: 11 ngày.

Thực tế, nhà nghiên cứu Tianyi Peng của Anthropic ban đầu không hề có ý định hoàn thành toàn bộ công việc này trong một lần.

Vốn là một học sinh xuất sắc trong các kỳ thi tin học từ sớm, Tianyi Peng từng giành giải tám trong kỳ thi chọn đội tuyển Olympic Tin học quốc gia, tốt nghiệp đại học tại Lớp Diệu (Yao Class) của Đại học Thanh Hoa năm 2017, và nhận bằng Tiến sĩ tại MIT năm 2023.

Hiện nay, anh là Giáo sư trợ lý tại Đại học Columbia, nhà nghiên cứu tại Anthropic, tập trung lâu dài vào học tăng cường (reinforcement learning), AI Agent và các công cụ hình thức hóa.

Khi bắt đầu, anh chỉ muốn thử nghiệm xem Claude có thể đẩy dự án này đi xa đến mức nào.