ETH là một phỏng đoán về độ khó vốn có của các bài toán khả thỏa: nói một cách khái quát, giả thuyết cho rằng không thể giải k-SAT (với k ≥ 3) trong thời gian 2o(n), trong đó n là số biến—tức là không có thuật toán nào giải được mọi trường hợp trong thời gian dưới hàm mũ theo n. Trên thực tế, ETH tạo ra một mốc chuẩn về độ khó: nhiều cận dưới có điều kiện cho các bài toán đồ thị, truy vấn cơ sở dữ liệu và các phép quy giản trong sinh học tính toán đều dựa trên ETH để lập luận rằng việc vượt qua một số mốc thời gian chạy nhất định sẽ là điều đáng ngạc nhiên. Khi các nhà nghiên cứu nói một bài toán khó theo ETH, ý họ là mọi cải thiện đáng kể đều hàm ý một bước đột phá vượt qua mốc chuẩn này.

Tuyên bố của OpenAI nhắm đến SAT độ rộng cố định: các trường hợp SAT bị giới hạn về cấu trúc mệnh đề hoặc tương tác giữa các biến. Nếu xây dựng được một thuật toán giải mọi trường hợp SAT độ rộng cố định trong thời gian 2o(n) (dưới hàm mũ theo n), điều đó sẽ mâu thuẫn với khẳng định bao quát của ETH về các cận dưới hàm mũ cho các họ k-SAT. Hệ quả ấy sẽ làm mất hiệu lực của nhiều kết quả về độ khó có điều kiện vốn dựa rõ ràng trên ETH. Điểm cốt yếu là bác bỏ ETH không đồng nghĩa với chứng minh P = NP: ETH là một phỏng đoán mạnh hơn, cụ thể hơn về mức độ phụ thuộc hàm mũ chính xác trong thời gian chạy. P = NP sẽ xóa bỏ khoảng cách giữa thời gian đa thức và thời gian đa thức không tất định; còn thuật toán dưới hàm mũ cho một họ SAT cụ thể chỉ cho thấy tốc độ tiệm cận nhanh hơn đối với họ đó, chứ không khẳng định có thể giải mọi bài toán NP trong thời gian đa thức.

Hình thức hóa một chứng minh bằng Lean là một bước có ý nghĩa: quá trình này buộc các định nghĩa phải chính xác, lấp nhiều khoảng trống trong lập luận không hình thức và tạo ra một kết quả có thể kiểm chứng bằng máy, giúp tránh một số dạng sai sót của con người. Nhóm OpenAI cho biết bản hình thức hóa Lean được hoàn tất trong vòng 24 giờ sau chứng minh bác bỏ bằng ngôn ngữ tự nhiên. Tuy vậy, kiểm chứng hình thức chỉ xác nhận tính đúng đắn về cú pháp dựa trên các tiên đề và định nghĩa hình thức; nó không thay thế việc cộng đồng diễn giải các giả định của mô hình, những hằng số ẩn trong phân tích tiệm cận, các miền tham số, hay việc thuật toán có áp dụng rộng rãi hay chỉ phù hợp với những họ trường hợp bệnh lý.

OpenAI mời một nhóm đánh giá do Russell Impagliazzo và Ramamohan Paturi—hai trong số những người đầu tiên đề xuất ETH—cùng Ryan Williams của MIT dẫn dắt. Bộ ba này kết hợp được bối cảnh lịch sử với thẩm quyền chuyên môn phù hợp: Impagliazzo và Paturi có thể xác định liệu lập luận bác bỏ được đề xuất có thực sự mâu thuẫn với cách phát biểu ETH ban đầu hay không, còn Williams có thể đánh giá hệ quả đối với các cận dưới thuật toán và những kết quả có điều kiện liên quan. Vai trò giám sát của họ sẽ giúp quá trình thẩm định kết quả minh bạch và do chuyên gia dẫn dắt, đồng thời nêu bật một mô hình hợp tác tích cực giữa công ty AI và giới học thuật.

Sự kiện này cho thấy một quy trình nghiên cứu mới: các mô hình tạo sinh có thể đề xuất phỏng đoán, thậm chí tạo ra chứng minh kiểm chứng được bằng máy, rút ngắn khoảng thời gian từ ý tưởng đến kết quả hình thức. Với các bên liên quan—nhóm nghiên cứu, nhà tài trợ và lãnh đạo sản phẩm—hàm ý chính sách trước mắt là cần đầu tư vào hạ tầng xác minh, kho lưu trữ mở cho các kết quả nghiên cứu và các đợt kiểm định do cộng đồng thực hiện với kinh phí hỗ trợ. Rủi ro vẫn còn: mô hình có thể tạo ra bổ đề sai nhưng vẫn vượt qua kiểm tra kiểu, áp dụng sai định nghĩa hoặc khai thác những giả định quá hẹp về trường hợp đầu vào. Cách ứng phó phù hợp không phải là tung hô thiếu suy xét hay bác bỏ theo phản xạ, mà là tiến hành xác minh có cấu trúc, minh bạch và do chuyên gia trong lĩnh vực dẫn dắt.