OpenAI công bố 719 bài toán học do AI viết, có cả lời giải Giả thuyết Unique Games: mới 42% được máy kiểm chứng

Tối 6/10/2026, OpenAI công khai một repository trên GitHub tên openai/math. Repository này chứa các kết quả toán học cấp nghiên cứu do một model nội bộ chưa phát hành tạo ra. Theo file README, kho gồm 719 bản thảo (manuscript), chia thành 372 “family”, tức nhóm kết quả. Mỗi nhóm gồm một kết quả chính và các bài đi kèm: hệ quả, lập luận bổ trợ hoặc cách chứng minh khác. Gây chú ý nhất là bản thảo The Unique Games Theorem. Nếu đúng, nó giải quyết giả thuyết có ảnh hưởng lớn nhất của lý thuyết độ phức tạp xấp xỉ (approximation complexity) kể từ khi Subhash Khot đề xuất năm 2002.

Tuần trước, blog này viết về sáu bài báo của Meta với Muse Spark. Ở đó, các nhà toán học có tên tuổi đã đọc hiểu kỹ kết quả của model trước khi công bố. OpenAI làm ngược lại: đưa ra cùng lúc hàng trăm chứng minh chưa ai thẩm định, rồi để cộng đồng tự sàng lọc. Scott Aaronson tóm gọn tâm trạng chung khi viết rằng gần như chưa có ai thực sự hiểu được các chứng minh này.

Nguồn gốc chính thức nói gì

README của repository mô tả phương pháp khá cụ thể:

Model: “một model nội bộ chưa phát hành của OpenAI”. OpenAI cho biết họ mở rộng việc đánh giá bằng các bài toán mở vì model đã đạt điểm tối đa trên các bộ benchmark (bộ bài kiểm tra chuẩn) toán học hiện có.
Tài nguyên tính toán: trung bình mỗi kết quả tốn khoảng ba giờ “suy nghĩ” ở mức ChatGPT Pro.
Quy mô: model được giao khoảng 4.000 bài toán. Đầu ra sau đó được gom thành các nhóm và lọc theo một ngưỡng “đủ quan trọng”.
Ngoại lệ: phần việc về miền không có nghiệm của hàm zeta Riemann và Giả thuyết Hodge cho đa tạp abel CM không theo quy trình chuẩn. Riêng bài về miền Re(s) > 11/12 được con người biên tập lại cho dễ đọc.
Tóm tắt quá trình suy luận: OpenAI công bố bản rút gọn quá trình suy luận cho 10 nhóm kết quả. Trong đó có số mũ vô tỷ của π, giả thuyết Kaplansky ở đặc số hai, và nhóm Unique Games.

Người phát ngôn của OpenAI nói với Scientific American rằng gần như mọi kết quả đều đến từ một prompt duy nhất giao cho một agent duy nhất, dù một số bài có thể phải thử nhiều lần. Cách làm này khác hẳn kết quả về phương trình Navier–Stokes hồi tháng 9, khi OpenAI dùng khoảng 10.000 agent cùng lúc.

“Đã kiểm chứng bằng Lean” thực ra nghĩa là gì

Lập trình viên nên đọc kỹ phần này. Lean là một trình trợ lý chứng minh (proof assistant). Khi một định lý biên dịch thành công trên nền thư viện mathlib, kernel của Lean đã kiểm tra từng bước logic. OpenAI kèm theo một thư viện Lean lớn và bộ file thử thách cho Comparator. Đây là công cụ thuộc tổ chức leanprover trên GitHub, dùng để đối chiếu một chứng minh với phát biểu định lý đã được cố định sẵn và con người đọc hiểu được. Ai cũng có thể tự chạy, ví dụ lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json trong thư mục lean/.

Có ba điểm cần lưu ý:

Mới kiểm chứng được một phần. Sau lần cập nhật ngày 7/10, file lịch sử của repository ghi “300 / 719 = ~42%” kết quả chính đã được hình thức hóa (formalize). Con số báo chí đưa ra dao động từ 162 đến 300, tùy thời điểm và cách đếm. Chính README thừa nhận các kết quả chưa hình thức hóa “có thể có vấn đề”.
Chứng minh hình thức chỉ bảo đảm phát biểu hình thức, chưa bảo đảm bài báo. Lấy ví dụ phần Unique Games. Thứ được hình thức hóa là một phép quy dẫn (reduction) tất định, thời gian đa thức, từ 3SAT sang các unique game hai phía trên bảng chữ cái 𝔽₂ˢ. Với mọi 0 < ε, δ < ½ cố định, ràng buộc là độ đầy đủ ≥ 1−ε và độ đúng ≤ δ. Đây là dạng NP-khó của giả thuyết. Còn phát biểu trong Lean có phản ánh đúng ý các nhà lý thuyết độ phức tạp hay không thì vẫn phải do con người đánh giá. Trong danh mục hình thức hóa của OpenAI, trường review: status vẫn ghi “unchecked” (chưa rà soát).
Lỗi đã bắt đầu lộ ra ở các bài không có chứng minh hình thức. Ngày 7/10, OpenAI rút ba bản thảo liên quan đến Giả thuyết Hodge vì một lỗi dấu làm hỏng lập luận triệt tiêu vết. Hãng cũng sửa 14 bài khác: vá chứng minh, chỉnh lại phát biểu và làm rõ giả thiết. Không bài nào trong số bị rút có chứng minh hình thức cho kết quả chính. Đây đúng là loại lỗi mà Lean sinh ra để bắt.

Bối cảnh của kết quả Unique Games

Giả thuyết Unique Games nói rằng với một loại trò chơi ràng buộc đặc biệt, rất khó phân biệt trường hợp gần như thỏa mãn được hết với trường hợp hầu như không thỏa mãn được gì. Giá trị của giả thuyết nằm ở các hệ quả. Nếu đúng, thuật toán Goemans–Williamson là tối ưu cho bài toán Max-Cut, và hệ số 2 là tối ưu cho Vertex Cover. Nhóm kết quả của OpenAI có bản thảo hình thức hóa riêng cho cả hai, cùng với Min-UnCut và bài toán tập đỉnh phản hồi có hướng.

Theo Quanta Magazine, một nhóm nghiên cứu đã chạy đua với máy. Tháng 9, Dor Minzer cùng hai học trò Yumou Fei và Shuo Wang nghe tin đồn OpenAI có chứng minh. Ba ngày sau, họ đăng bài báo 95 trang chứng minh phiên bản yếu hơn (4-to-1), khép lại khoảng bảy năm nghiên cứu. Dana Moshkovitz cũng đã theo đuổi giả thuyết này nhiều năm. Bà nói bài của OpenAI viết tệ đến mức không có AI hỗ trợ thì “không thể” đọc nổi. Sau đó bà cho Aaronson biết mình đã hiểu phần lớn bài nhờ AI. Mark Braverman (Princeton) nhận xét thẳng: “Làm toán bằng thông cáo báo chí không tốt cho toán học.”

Vì sao chuyện này quan trọng với ngành IT

Với ngành IT, con số đáng chú ý không phải 372 mà là ba giờ tính toán mức Pro cho mỗi kết quả. Tìm chứng minh ở cấp nghiên cứu giờ giống một khối lượng công việc inference (chạy model) bình thường: có thể lên lịch, chạy song song và lập ngân sách. Trong khi đó, phần kiểm chứng ngày càng giống kỹ thuật phần mềm. Có một monorepo, một bản build có thể thất bại nếu tham số vm.max_map_count của Linux đặt quá thấp, một đặc tả cho từng định lý, và một công cụ kiểm tra kiểu CI. Các đội phần mềm cũng đang gặp đúng sự phân tách này với coding agent: viết ra thì ngày càng rẻ, nên điểm nghẽn chuyển sang khâu đặc tả và review. Ba bài Hodge bị rút cho thấy chuyện gì xảy ra khi một kết quả được công bố mà không có đặc tả kiểm chứng bằng máy.

Còn một khía cạnh bảo mật. Aaronson lưu ý mật mã học vắng mặt một cách đáng ngờ trong danh sách, và các phòng lab đang âm thầm thử xem model có phá được các thuật toán mật mã nền tảng hay không. OpenAI chưa báo cáo kết quả nào như vậy. Dù vậy, một model tuyên bố đạt các kết quả như L = BPL hay chặn dưới mới cho mạch logic, mỗi bài chỉ tốn vài giờ tính toán, là chuyện đáng lưu tâm với bất kỳ ai đang lên lộ trình chuyển sang mật mã hậu lượng tử.

Những câu hỏi còn bỏ ngỏ

Khả năng tái lập. Ngày 21/9, OpenAI lập một nhóm cố vấn gồm các nhà toán học. Nhóm khuyến nghị công bố model, prompt chính xác và lượng tài nguyên tính toán cho từng kết quả. OpenAI mới chỉ công bố số trung bình và 10 bản tóm tắt suy luận. Hãng nói nghiêm túc xem xét các hướng dẫn nhưng “không bị ràng buộc” bởi chúng. Andrew Sutherland (MIT) nói: “Chúng ta nên đòi xem bằng chứng.” Chừng nào model chưa được phát hành, tuyên bố “một prompt, một agent” vẫn chưa thể kiểm tra.
Cách chọn lọc. README không nêu số bài thất bại, cũng không định nghĩa ngưỡng “đủ quan trọng”. Vì vậy không thể suy ra tỷ lệ thành công rõ ràng từ con số khoảng 4.000 bài được giao.
Ghi công và cộng đồng. Association for Human Mathematics kêu gọi các nhà toán học ngừng hợp tác với OpenAI. Terence Tao gọi tốc độ ra kết quả của các phòng lab là “điên rồ”. Ngược lại, Daniel Litt cho rằng đợt công bố sẽ có lợi cho toán học. Khác với cách Meta hay Anthropic tự biên tập kết quả trước khi công bố, lần này phần việc đọc hiểu và thẩm định dồn sang những người ngoài, không được trả công.

Đánh giá công bằng nhất có lẽ là: những phần đã được máy kiểm chứng trong đợt công bố này đã có ý nghĩa thật sự. Phần còn lại giống một kho preprint (bản thảo chưa bình duyệt) khổng lồ, ra đời rất nhanh và chỉ có một tác giả. Vài tháng bình duyệt sắp tới sẽ cho thấy phần nào đứng vững.