Lean Theorem Prover: Khi AI viết chứng minh toán học và câu hỏi về độ tin cậy

Toán học từ lâu được xem là nền tảng đáng tin cậy nhất của khoa học và văn minh nhân loại. Nhưng khi trí tuệ nhân tạo bắt đầu tham gia vào việc chứng minh các định lý, câu hỏi về độ tin cậy của chính nền tảng đó lại trở nên cấp thiết hơn bao giờ hết. Bài viết của Thomas Hales trên blog của Terence Tao — một trong những nhà toán học có ảnh hưởng nhất thế giới — đã đặt vấn đề này một cách thẳng thắn.

Lean là gì và vì sao nó quan trọng?

Lean là một trợ lý chứng minh (proof assistant) được Leo de Moura phát triển năm 2013 tại Microsoft, sau đó được mã nguồn mở hóa. Đây là một hệ thống phần mềm cho phép các nhà toán học viết định nghĩa, phát biểu định lý và chứng minh chúng theo cách mà máy tính có thể kiểm tra từng bước một.

Điểm đặc biệt của Lean nằm ở chỗ nó không chỉ là công cụ kiểm tra logic thuần túy. Hệ thống này kết hợp ngôn ngữ lập trình đa dụng với ngôn ngữ toán học trong cùng một môi trường. Các chứng minh sau khi được viết ra sẽ trải qua quá trình elaboration (biên dịch toán học) rồi được kernel — lõi kiểm tra vài nghìn dòng C++ — xác minh độc lập.

Thư viện toán học của Lean, gọi là mathlib, hiện chứa gần 300.000 định lý, hơn 100.000 định nghĩa và 2,5 triệu dòng mã, với hơn 700 người đóng góp. Nhiều định lý lớn đã được hình thức hóa thành công, bao gồm định lý bốn màu, định lý Feit-Thompson, giả thuyết Kepler, bài toán xếp cầu trong không gian 8 và 24 chiều, và gần đây nhất là Định lý cuối cùng của Fermat.

Autoformalization: Khi AI viết chứng minh

Nếu trước đây việc chuyển chứng minh trên giấy sang mã Lean phải làm thủ công — dự án hình thức hóa giả thuyết Kepler tốn khoảng 20 năm công lao động người với 500.000 dòng — thì năm 2026 đánh dấu bước ngoặt với autoformalization, tức để AI tự động đọc bài báo toán học và xuất ra chứng minh Lean.

Một số cột mốc đáng chú ý:

• Tháng 9/2025: Math Inc. tạo ra bản bán tự động hóa định lý số nguyên tố, dù vẫn cần con người can thiệp khi AI bị kẹt.
• Tháng 1/2026: J. Urban công bố preprint "130k dòng topology hình thức trong hai tuần".
• Tháng 3/2026: Math Inc. tự động hóa bài toán xếp cầu 24 chiều, tạo ra khoảng 500.000 dòng mã, sau đó rút gọn còn 200.000 dòng.
• Tháng 5/2026: Nhóm Meta/Facebook Research tự động hóa phần lớn 26 cuốn sách giáo khoa toán trong dự án ATLAS.
• Tháng 9/2026: Anthropic công bố autoformalization Định lý cuối cùng của Fermat với 13 triệu dòng Lean trong 11 ngày. OpenAI cũng công bố autoformalization định lý Navier-Stokes có nhiễu.

"Chúng tôi tin rằng (tự động) hình thức hóa có thể trở nên khá dễ dàng và phổ biến vào năm 2026, bất kể dùng trợ lý chứng minh nào." — J. Urban

Jared Lichtman thậm chí đã khởi động dự án MAP (Mathematics Autoformalization Project) với tham vọng dịch "toàn bộ toán học đã biết thành mã hình thức" — và mời gọi mọi người hình dung về nghìn tỷ dòng mã tiếp theo.

Mùa hè của những lỗi soundness

Vấn đề nằm ở chỗ: soundness bug — lỗi trong kernel cho phép chứng minh mệnh đề "Sai" và do đó chứng minh được mọi thứ — là loại lỗi tai hại nhất trong một trợ lý chứng minh. Và mùa hè 2026 đã chứng kiến một loạt lỗi như vậy trong Lean.

Một lỗi thậm chí dẫn đến chứng minh sai cho giả thuyết Collatz. Thomas Hales biết đến lỗi này khi nó tạo ra một chứng minh ngắn bất hợp lệ cho giả thuyết Kepler. Tất cả các lỗi đều được sửa nhanh chóng, và mathlib đã được kernel đã vá xác minh lại.

Điều đáng chú ý: các lỗi này được phát hiện bởi AI tiên tiến trong tay các nhà nghiên cứu bảo mật, không phải bởi hacker mũ đen. Ramana Kumar — đồng tác giả của CakeML — tìm ra lỗi Collatz. Dan Selsam tại OpenAI đã hỗ trợ Lean FRO với một AI chuyên về an ninh mạng để tìm thêm các lỗi lập trình khác trong kernel.

Ba hướng giải quyết

Thomas Hales đề xuất ba cách tiếp cận để giảm thiểu rủi ro soundness bug:

1. Phát triển kernel Lean khác và kiểm tra chéo. Khoảng 25 kernel cho Lean đã được viết, được liệt kê trong "Lean Kernel Arena". Bản hình thức hóa Navier-Stokes đã được xác nhận bởi hơn một chục trình kiểm tra khác nhau. Tuy nhiên, việc kiểm tra chéo không loại bỏ hoàn toàn nghi ngờ — lỗi Collatz đã không bị phát hiện bởi kernel Nanoda vì nó có lỗi riêng không liên quan.

2. Xác minh hình thức kernel. Đây là hướng đi đáng chú ý nhất. Joachim Breitner đã phát triển Con-Leche, một kernel Lean đã được xác minh với chứng minh nhất quán hình thức, sử dụng Claude để sinh mã và chứng minh. Con-Leche đã kiểm tra mathlib và chứng minh nhất quán của nó đã được hơn một chục trình kiểm tra khác xác nhận.

3. Cải thiện hiểu biết lý thuyết về kernel và lý thuyết kiểu của Lean. Đây có lẽ là điểm yếu lớn nhất. Mario Carneiro đã chỉ ra rằng định nghĩa bằng nhau trong Lean là không thể quyết định — nghĩa là thuật toán Lean không thể thiết lập tính bằng nhau định nghĩa của một số hạng tử dù chúng thực sự bằng nhau. Nhiều câu hỏi cơ bản khác vẫn chưa có lời giải, bao gồm unique typing, Pi-injectivity và tính nhất quán logic tương đối với lý thuyết tập hợp.

Góc nhìn từ Việt Nam

Đối với cộng đồng nghiên cứu và sinh viên toán học tại Việt Nam, sự phát triển của Lean và autoformalization mở ra cả cơ hội lẫn thách thức. Một mặt, các công cụ này giúp việc học và kiểm chứng toán học trở nên dễ tiếp cận hơn — bất kỳ ai có máy tính và kết nối internet đều có thể thử sức với mathlib. Mặt khai, việc phụ thuộc vào các hệ thống AI phức tạp đặt ra câu hỏi về chủ quyền công nghệ và năng lực kiểm toán độc lập.

Bài học từ "Reflections on Trusting Trust"

Thomas Hales kết thúc bằng cách nhắc lại bài luận nổi tiếng năm 1984 của Ken Thompson: "Bạn không thể tin tưởng mã nguồn mà bạn không hoàn toàn tự tạo ra... Không lượng xác minh hay soi xét nào ở cấp mã nguồn có thể bảo vệ bạn khỏi việc sử dụng mã không đáng tin."

Trong thời đại AI, câu hỏi này trở nên sâu sắc hơn: làm sao chứng nhận rằng AI đã không để lại một backdoor soundness bug trong Lean khi nó quét lỗi vào mùa hè 2026? Điều gì xảy ra nếu lỗi đó bị khai thác để cài backdoor vào phần mềm đã được xác minh hình thức, bảo vệ hạ tầng trọng yếu?

"Trong năm qua, nhiều công trình nền tảng về cơ sở lý thuyết kiểu của toán học và độ tin cậy của nó đã được giao phó cho AI, và điều này nguy hiểm trừ khi được con người kiểm toán cẩn thận." — Thomas Hales

Đây không chỉ là câu chuyện kỹ thuật của giới toán học. Khi AI ngày càng tham gia sâu vào việc xác minh các hệ thống quan trọng — từ phần mềm tài chính đến cơ sở hạ tầng — câu hỏi về việc ai kiểm tra người kiểm tra trở thành vấn đề sống còn. Thomas Hales kết luận rằng tác giả bài viết hoàn toàn là con người, AI chỉ được dùng như công cụ tìm kiếm, kiểm chứng thông tin và hiệu đính — một tuyên bố đáng suy ngẫm trong thời đại mà danh giới giữa sáng tạo người và máy ngày càng mờ nhạt.