Formal hóa toàn bộ toán học: Cơ hội lớn hay thảm họa tiềm tàng?

Sự phát triển vượt bậc của AI trong việc chứng minh định lý đang làm dấy lên làn sóng kêu gọi formal hóa toàn bộ toán học. Tuy nhiên, một nhóm các nhà toán học hàng đầu cảnh báo rằng nếu thực hiện vội vã và thiếu quy chuẩn, nỗ lực này có thể gây lãng phí hàng triệu đô la và làm tổn hại nghiêm trọng đến ngành toán học trong nhiều thập kỷ.

Trong một bài viết khách mời trên blog Xena Project, các tác giả Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash và Adam Topaz đã chia sẻ góc nhìn sâu sắc về vai trò của AI trong việc hình thức hóa toán học. Họ thừa nhận sức mạnh của công nghệ mới nhưng đồng thời bày tỏ lo ngại về những lời kêu gọi formal hóa mọi thứ càng nhanh càng tốt.

Khi hình thức hóa trở thành gánh nặng

Điểm mấu chốt mà các tác giả nhấn mạnh: một sản phẩm hình thức hóa không có giá trị nếu không ai sử dụng nó.

Họ dẫn chứng trường hợp Math, Inc. cố gắng chiếm đoạt dự án formal hóa kết quả đóng gói hình cầu đa chiều của Maryna Viazovska. Dù chứng minh được sức mạnh của công nghệ, dự án này không đóng góp gì cho toán học. Nhóm nghiên cứu gốc sau đó phát hiện rằng việc dọn dẹp mã do AI tạo ra còn tốn công hơn là viết lại từ đầu.

Tương tự, khi Anthropic công bố Claude đã xác minh hình thức Định lý cuối cùng của Fermat với 13 triệu dòng mã viết trong 11 ngày, Kevin Buzzard đã khen ngợi thành tựu này nhưng tuyên bố ông không có ý định dừng công việc formal hóa của mình theo một chứng minh hiện đại hơn. Một lần nữa, mã do AI tạo ra có thể có rất ít giá trị lâu dài.

"Chúng ta muốn hình thức hóa mọi thứ vì chúng ta muốn sử dụng các hình thức hóa để làm toán nhiều hơn, và làm tốt hơn so với khi không có chúng."

Các tác giả giải thích rằng giá trị thực sự của việc hình thức hóa không nằm ở tính đúng đắn đơn thuần, mà ở khả năng sử dụng và tương tác với dữ liệu. Họ muốn khám phá các tổng quát hóa, tìm mối liên hệ giữa các nhánh toán học khác nhau, và tái cấu trúc kiến thức để làm cho các khái niệm trở nên thanh lịch và hiệu quả hơn.

Những mặt tích cực

Không phải mọi nỗ lực của các phòng thí nghiệm lớn đều thất bại. Các tác giả đánh giá cao công trình về giả thuyết khoảng cách đơn vị của OpenAI và công trình về mật độ các điểm không của hàm zeta Riemann của Anthropic. Những kết quả này thể hiện khả năng mới ấn tượng, đóng góp vào hiểu biết và được cộng đồng tiếp tục phát triển.

Trong tương lai, các thư viện hình thức hóa chất lượng cao sẽ cho phép con người, AI và ngôn ngữ Lean phối hợp chặt chẽ. AI sẽ tạo ra các chứng minh hình thức trong khi làm việc, liên tục kiểm tra chúng với trình biên dịch Lean và tự động loại bỏ các lập luận sai.

Các dự án tiêu biểu đang định hình tương lai

Bài viết giới thiệu một số dự án quan trọng đang xây dựng nền tảng cho hệ sinh thái hình thức hóa toán học:

• Mathlib: Thư viện mã nguồn mở do cộng đồng dẫn dắt, được giám tuyển bởi 65 người đánh giá và 950 người đóng góp. Nhấn mạnh chất lượng cao và sự giám tuyển của con người, phát triển chậm nhưng ổn định.

• Formal Conjectures: Nỗ lực hợp tác thu thập các phát biểu hình thức của những bài toán mở. Đây là một doanh nghiệp xã hội đòi hỏi thảo luận, đánh giá và kiểm toán.

• Annals Challenge: Dự án do Kevin Buzzard dẫn đầu nhằm phát biểu (không chứng minh) tất cả định lý từ các số gần đây của tạp chí Annals of Mathematics.

• Tau Ceti: Thư viện toán học hình thức lớn, được ươm tạo bởi Lean FRO và Mathlib Initiative. Tất cả đóng góp do AI viết và được AI khác phản biện. Hiện có 3 triệu dòng mã, lớn hơn Mathlib một chút.

• Formal Frontier: Dự án xây dựng đường ống chuyển đổi văn bản nguồn thành các thư viện hình thức liên kết. Có 41 thư viện đã phát hành với khoảng 200.000 dòng mã.

• Palomar: Cơ quan đăng ký trực tuyến các dự án toán học hình thức, yêu cầu tệp metadata formalization.yaml và thiết lập Comparator để dễ kiểm toán.

Bộ giá trị chung

Các thư viện này chia sẻ những nguyên tắc chung, không chỉ riêng cho autoformalization mà cho mọi thư viện hình thức hóa:

• Tôn trọng thư viện do con người giám tuyển, đặc biệt là Mathlib, tuân theo nguyên tắc thiết kế và quy tắc mã của họ
• Ưu tiên tính kỹ lưỡng và độ rộng trước khi đi vào chiều sâu
• Tránh trùng lặp, tổng quát hóa định lý để tái sử dụng tối đa
• Đánh giá công khai các bổ sung theo tiêu chuẩn đã thống nhất
• Xuất bản tự do, mã nguồn mở và có thể khám phá
• Cập nhật liên tục với mọi phiên bản Lean và Mathlib
• Ghi chép và tổ chức tài liệu một cách hệ thống
• Đặt ra tiêu chuẩn và đáp ứng chúng — sản xuất mã chất lượng thấp rồi hy vọng "dọn dẹp sau" là phản tác dụng

Con đường phía trước

Các tác giả tin rằng trong vòng ba năm, phần lớn toán học có thể được hình thức hóa theo cách mà các nhà toán học có thể khám phá, xây dựng và sử dụng. Để đạt được điều này, cần:

• Giám tuyển và đóng góp cho Mathlib
• Cung cấp nguồn lực để Tau Ceti và Formal Frontier mở rộng gấp mười lần trong vài tháng
• Viết lộ trình chuyên gia hướng dẫn triển khai các thư viện hình thức lớn
• Phát triển mô hình hóa tài chính, kỹ thuật và kỹ thuật cho việc mở rộng quy mô
• Vận động để các nhà toán học kiểm soát các công cụ và nguồn lực cần thiết
• Khởi động dịch vụ lưu trữ phi lợi nhuận hoặc học thuật với quản trị phù hợp

"Một thất bại lớn sẽ khiến việc phục hồi sau này trở nên khó khăn, thậm chí bất khả thi. Một hình thức hóa tồi của các kết quả hiện có còn tệ hơn là không hình thức hóa gì cả."

Đối với cộng đồng công nghệ Việt Nam đang ngày càng quan tâm đến AI và ứng dụng trong nghiên cứu, bài học từ ngành toán học này mang tính cảnh báo quan trọng: sức mạnh của AI không thay thế được sự giám tuyển của con người, chất lượng dữ liệu và tầm nhìn dài hạn. Việc triển khai AI trong bất kỳ lĩnh vực nào — từ phần mềm đến tài chính, y tế — đều cần cân nhắc giữa tốc độ và chất lượng, giữa tự động hóa và giá trị con người.