AI của OpenAI và Anthropic cùng tuyên bố bác bỏ Giả thuyết Thời gian Mũ: thuật toán SAT mới chứng minh được gì, chưa chứng minh được gì

Suốt gần 25 năm, khoa học máy tính lý thuyết dựa vào một giả định mà hầu như không ai nghĩ sẽ đổ: bài toán 3-SAT không thể giải trong thời gian 2^o(n). Tuần này, hai phòng lab AI cùng nói model của họ đã bác bỏ giả định đó, một cách độc lập, và cả hai đều ghi bước then chốt được tìm ra trong cùng một ngày.

Thứ Hai, 26/10/2026, OpenAI công bố một loạt kết quả do “một model nội bộ không nêu tên” tạo ra. Nổi bật là ba tuyên bố. Thứ nhất là bác bỏ Giả thuyết Thời gian Mũ (Exponential Time Hypothesis, ETH). Thứ hai là chứng minh giả thuyết local smoothing trong giải tích điều hòa, kéo theo các giả thuyết Kakeya và Stein restriction. Thứ ba là chứng minh sự tồn tại của lý thuyết Yang–Mills và QCD trong bốn chiều. Chỉ vài giờ sau, Anthropic đưa lên máy chủ preprint Hexagon bài báo “A 2^o(n) Time Algorithm for 3-SAT” (phiên bản 1 đề ngày 27/10). Phần ghi nguồn gốc viết: thuật toán cốt lõi “được một model Claude nghiên cứu nội bộ tìm ra ngày 16/10, với 14 triệu token đầu ra và không có sự tham gia của con người”. OpenAI cũng ghi ngày tìm ra lời bác bỏ ETH là 16/10, và hoàn tất bản hình thức hóa bằng Lean ngay hôm sau.

Bài này tập trung vào ETH. Đây là kết quả gần với dân lập trình nhất, và là kết quả mà cả hai bên đều đã công bố tài liệu để người ngoài tự kiểm tra.

ETH là gì, vì sao quan trọng

ETH do Russell Impagliazzo và Ramamohan Paturi đề xuất khoảng năm 2000, cùng Francis Zane ở bài báo đi kèm. Nói nôm na, tồn tại một hằng số δ > 0 sao cho không thể giải 3-SAT trên n biến trong thời gian 2^δn. SAT không chỉ khó mà khó theo hàm mũ: không thuật toán thông minh nào hạ được số mũ xuống mức nhỏ hơn tuyến tính theo n. Các thuật toán tốt nhất hiện nay cho 3-SAT chạy cỡ 1,3ⁿ trong trường hợp xấu nhất, tức vẫn là hàm mũ, phù hợp với ETH.

ETH mạnh hơn P ≠ NP, và chính vì vậy mà nó hữu ích. Hàng trăm kết quả trong độ phức tạp tham số hóa và độ phức tạp “hạt mịn” (fine-grained, ngành đo độ khó chính xác tới từng số mũ) là cận dưới có điều kiện, dạng “nếu ETH đúng thì bài toán X không có thuật toán 2^o(k)”. Khi muốn chứng tỏ thuật toán mũ của mình cho một bài toán đồ thị là gần tối ưu, các nhà nghiên cứu thường dựa vào ETH. Nếu ETH sai, những kết quả đó không thành sai, nhưng chúng thành mệnh đề suy ra từ một tiền đề sai và không còn cho biết điều gì.

Hai bên thực sự tuyên bố gì

OpenAI. Tài liệu mô tả phạm vi chứng minh Lean trong kho GitHub công khai openai/math ghi: với mọi k ≥ 2 cố định, một máy tất định đếm chính xác số phép gán thỏa mãn của công thức k-CNF trên n biến trong thời gian (L+1)^O_k(1) · 2^{O_k(n (log log n)² / √log n)}, với L là độ dài đầu vào tính theo bit, và chỉ dùng bộ nhớ đa thức. Bản thảo ngày 25/10 nêu số mũ chặt hơn, n·log log n / √log n, và đạt 2^{O(n/√log n)} khi tỉ lệ mệnh đề trên biến bị chặn. Các bên theo dõi tuyên bố này lưu ý rằng định lý Lean chỉ bao phủ cận yếu hơn. Các cận chặt hơn mới chỉ dựa trên chứng minh viết tay.

Anthropic. Phần tóm tắt rất ngắn: thuật toán tất định giải 3-SAT trên n biến trong thời gian 2^o(n), thực chất giải luôn bài toán khó hơn là #3-SAT (đếm nghiệm), và đã được hình thức hóa bằng Lean 4. Trang bài báo gắn nhãn “văn bản chủ yếu do AI viết” và “con người hiểu được một số phần”. Bài cũng ghi nhận OpenAI tuyên bố một kết quả tương tự.

Có hai chi tiết đáng chú ý với lập trình viên. Một là cả hai thuật toán đều đếm nghiệm chứ không chỉ trả lời có nghiệm hay không. Đếm khó ít nhất bằng quyết định, nên đây là tuyên bố mạnh hơn. Hai là cả hai đều tất định, không dùng ngẫu nhiên nên không có chỗ để tranh cãi về xác suất.

Lean chứng nhận được gì, không chứng nhận được gì

Lean là ngôn ngữ và công cụ kiểm chứng chứng minh toán học bằng máy. Một chứng minh Lean biên dịch thành công nghĩa là phát biểu hình thức suy ra được từ hệ tiên đề và thư viện. Nó không đảm bảo phát biểu hình thức đó đúng là định lý mà ta nghĩ. Mô hình máy tính có thể bị định nghĩa lệch một chút. Cách mã hóa đầu vào có thể ngầm thêm giả thiết. Cận thời gian trên bản PDF có thể mạnh hơn cận mà Lean thực sự kiểm tra, và khoảng cách này đã có thật ở phía OpenAI. Vì vậy hình thức hóa là cần nhưng chưa đủ, và vẫn phải có chuyên gia đọc từng dòng phát biểu.

Còn một vấn đề nữa. OpenAI tự mô tả toàn bộ đợt công bố (721 bản thảo thuộc 373 nhóm, rút từ khoảng 4.000 bài toán, trung bình mỗi kết quả tốn ba giờ suy luận ở mức ChatGPT Pro) là “dữ liệu nghiên cứu thô, không phải bài báo học thuật hoàn chỉnh”, và cảnh báo “một số kết quả chưa hình thức hóa có thể có vấn đề”. Sự thẳng thắn đó đáng ghi nhận. Nhưng nó cũng có nghĩa gánh nặng thẩm định đã chuyển sang cộng đồng nghiên cứu.

Không đổi gì với SAT solver của bạn, nhưng có thể đổi nhiều với lý thuyết

Cận 2^{n/√log n} là dưới mũ (subexponential), nhưng vẫn lớn hơn mọi đa thức. Các hằng số ẩn trong ký hiệu O_k(·) chưa được công bố và nhiều khả năng rất lớn. Các bài phân tích đều đồng ý rằng thuật toán không cho tăng tốc thực tế ở bất kỳ kích thước nào máy tính xử lý được. SAT solver kiểu CDCL, bộ giải phụ thuộc của trình quản lý gói hay công cụ kiểm chứng dùng SMT đều không bị ảnh hưởng. Mật mã không bị phá. Các hệ mật mã đang dùng không dựa vào ETH, và không nguồn nào cho rằng có ảnh hưởng. Bác bỏ ETH cũng không giải quyết bài toán P vs NP.

Tác động thật nằm ở lý thuyết. Nếu kết quả đứng vững, mọi cận dưới dựa trên ETH sẽ cần một nền móng mới, chẳng hạn các giả thuyết yếu hơn hoặc giả thuyết về bài toán khác, và giới nghiên cứu sẽ phải rà xem kết quả nào còn giữ được. Đây cũng sẽ là lần đầu một cỗ máy tự lật đổ một giả thuyết nền tảng của lý thuyết độ phức tạp, chứ không chỉ là con người lật đổ với sự trợ giúp của máy. Việc hai phòng lab độc lập cùng đi tới kết quả trong một tuần khiến khả năng “ăn may” thấp hơn.

Sự thận trọng là có chủ đích

Ba người có thẩm quyền nhất để đánh giá kết quả là chính các tác giả của ETH, Impagliazzo và Paturi (UC San Diego), cùng Ryan Williams (MIT). Họ đang điều phối việc thẩm định và viết: “Việc chúng tôi tham gia không nên được hiểu là xác nhận tuyên bố. Một kết quả tầm cỡ này cần được xem xét kỹ lưỡng và độc lập.” OpenAI đồng ý công bố dữ liệu thô và tài trợ một hội nghị về kết quả này. Riêng rẽ với hai việc đó, OpenAI tặng 5 triệu USD cho Quỹ Simons để tổ chức hội thảo về toán học do AI tạo ra.

Hai tuyên bố còn lại kém vững hơn. Chứng minh local smoothing đã công khai, và nhà giải tích điều hòa Alex Iosevich gọi đó là “bước phát triển lịch sử”. Tuy vậy, phạm vi hệ quả về Kakeya và Stein được mô tả khác nhau ngay trong các câu của chính OpenAI. Kết quả Yang–Mills/QCD ít tài liệu nhất. Nhóm do David Gross dẫn dắt đang tự viết lại và chưa công bố tài liệu gốc của AI, nên Timothy Gowers cùng Nhóm Tư vấn về Toán học và AI (AGMAI) đã công khai yêu cầu OpenAI công bố. Đây cũng chỉ là kết quả về sự tồn tại. Chưa tài liệu nào công bố tuyên bố giải được “khe khối lượng” (mass gap), vốn mới là bài toán thiên niên kỷ thực sự của Viện Clay.

Tính đến hôm nay, chưa có kết luận thẩm định độc lập nào được công bố cho cả ba kết quả. Cách hiểu đúng là “tuyên bố rất nghiêm túc, kèm tài liệu để kiểm tra”, chưa phải “định lý”.

Cần theo dõi gì tiếp

Kết luận của nhóm Impagliazzo–Paturi–Williams, và liệu cận chặt hơn trong bản thảo có được hình thức hóa bằng Lean hay không.
Hai thuật toán có chung ý tưởng cốt lõi không. Nếu có, chỉ một lỗi là cả hai cùng đổ. Nếu khác nhau, đó là bằng chứng củng cố mạnh.
Việc công bố tài liệu Yang–Mills, và cách các tạp chí cũng như arXiv xử lý toán học “chủ yếu do AI viết”.
Tốc độ OpenAI và Anthropic đưa loại model nghiên cứu này thành sản phẩm. Câu “14 triệu token đầu ra, không có con người tham gia” là chi tiết mà người quản lý kỹ thuật nên nhớ.