Nhà toán học phản bác OpenAI trong 24 giờ: AI chứng minh đúng từng câu nhưng lại sai lệch hoàn toàn so với giả thuyết gốc

< img id="wx_img" src="https://www.qbitai.com/wp-content/uploads/imgs/qbitai-logo-1.png" width="400" height="400">

04-08-2026 17:22:46 Nguồn: QbitAI

Ngay ngày hôm sau, một bài báo của con người đã phản hồi: Phản ví dụ do AI đưa ra không chính xác.

Meng Chen, đưa tin từ QbitAI | Tài khoản chính thức QbitAI

OpenAI tuyên bố mô hình AI thế hệ tiếp theo đã giải quyết được 10 bài toán hóc búa tầm cỡ thế giới, trong đó có việc bác bỏ Giả thuyết cứng Connes (Connes rigidity conjecture).

Ngay ngày hôm sau, một bài báo của con người đã phản hồi: Phản ví dụ do AI đưa ra không chính xác.

Tác giả là J. L. Nielsen từ Trung tâm Vật lý Tô pô thuộc Đại học Kansas. Cô đã rà soát toàn bộ 37.000 dòng mã Lean 4 mà OpenAI công khai, đối chiếu từng đối tượng với nguyên mẫu toán học của nó và cuối cùng đưa ra hai lộ trình thất bại độc lập.

Quy trình chứng minh cụ thể thì người bình thường như chúng ta khó mà hiểu được, cứ để AI và các nhà toán học "đấu đá" với nhau vậy.

Tuy nhiên, sự việc này cho thấy việc con người kiểm chứng các kết quả nghiên cứu khoa học của AI vẫn là điều vô cùng quan trọng.

Giả thuyết cứng Connes là gì?

Giả thuyết cứng Connes đề cập đến vấn đề sau đây.

Trong toán học, người ta có thể gán một cấu trúc đại số cho một nhóm (group). Đôi khi, hai nhóm trông có vẻ khác nhau nhưng cấu trúc được gán lại hoàn toàn giống hệt nhau.

Khoảng năm 1980, Connes đưa ra giả thuyết: Chỉ cần nhóm này thỏa mãn hai điều kiện bổ sung, tình trạng trên sẽ không xảy ra; nếu cấu trúc giống nhau thì các nhóm bắt buộc phải giống nhau.

Hai điều kiện bổ sung đó, một là ICC, hai là tính chất Kazhdan (T).

Nói cách khác, để bác bỏ giả thuyết này, cần phải đưa ra được các nhóm thỏa mãn cả hai điều kiện nhưng có cấu trúc khác nhau.

Cách làm của mô hình mới từ OpenAI là xây dựng hai nhóm không đẳng cấu, khiến chúng tạo ra cùng một đại số, đồng thời đưa ra chứng minh rằng cả hai nhóm đều thỏa mãn ICC và tính chất (T).

Toàn bộ lập luận được viết thành 37.000 dòng mã Lean 4, được nhân (kernel) của Lean xác minh từng dòng một, kèm theo một tài liệu giải thích cách thức xây dựng hai nhóm này.

Nielsen chỉ ra rằng: Một trong hai nhóm mà AI xây dựng thực tế không thỏa mãn các điều kiện bổ sung, nó không phải là ICC, cũng không có tính chất (T).

Có ba khả năng xảy ra:

Tính chất (T) trong mã nguồn không tương ứng chính xác với định nghĩa gốc của Kazhdan; hoặc chứng minh chỉ đúng với một phần nhưng lại bị áp đặt cho toàn bộ nhóm; hoặc nhóm trong mã nguồn hoàn toàn không giống như mô tả trong tài liệu hướng dẫn.

37.000 dòng, đối chiếu từng dòng một

Để xác minh kết luận này, Nielsen đã thực hiện một công việc tốn công sức hơn nhiều.

Mã nguồn được công bố là phiên bản đã hợp nhất thành một tệp duy nhất, tất cả tên gọi trong các module nguồn ban đầu đều đã biến mất.

Vì vậy, cô đã lập một bảng đối chiếu, đánh dấu tên và số dòng của từng đối tượng toán học trong mã mới:

Nhóm chuỗi đóng bậc không (zero-degree closed chain group) ở dòng 13700, nhóm xoắn (twist group) ở dòng 14069, chứng minh hai đại số đẳng cấu ở dòng 36712, định lý chính ở dòng 36954.

Cô cũng đã truy vết toàn bộ chuỗi suy luận chứng minh ICC của mã nguồn. Chuỗi này bắt đầu từ dòng 31430, truyền dẫn qua từng lớp và cuối cùng tổng hợp thành kết luận ở dòng 31610.

Vấn đề mà Nielsen chỉ ra là các bổ đề này xử lý các đối tượng sau khi đã qua biến đổi đối ngẫu, chứ không phải nhóm gốc có chứa phần tử trung tâm, do đó nó không bao phủ trực tiếp phần tử then chốt đó.

Việc chúng có đúng với từng phần tử trong nhóm cụ thể cuối cùng được đưa vào định lý hay không còn phụ thuộc vào cách kết nối giữa hai khối cấu trúc.

Điều này cho thấy vấn đề nằm ở chỗ "cần chứng minh cái gì", chứ không phải "chứng minh đúng hay sai". Lean chỉ chịu trách nhiệm xác minh vế sau.

Đối với nhóm xoắn còn lại, thái độ của Nielsen khá thận trọng. Cô cho biết mình chưa thể xác minh độc lập từ mã nguồn xem nó có thực sự thỏa mãn ICC hay không, đồng thời thừa nhận các bổ đề trong mã có thể đã chứng minh được điều đó, nhưng điều đó không thay đổi kết luận vì đã có một nhóm không thỏa mãn.

Cô cũng đã viết các phản biện của mình thành mã Lean và biên dịch thành công trên Lean 4.32.2.

Máy móc kiểm tra hình thức, không phải ý nghĩa

Phần cuối của bài báo đã đặt sự việc này vào một bối cảnh rộng lớn hơn.

Những gì nhân Lean có thể đảm bảo chỉ là một chứng minh chặt chẽ về mặt hình thức, nhưng nó không chịu trách nhiệm về việc liệu chứng minh đó có thực sự chứng minh được kết luận ban đầu hay không.