Mô hình lập luận mới nhất nội bộ của OpenAI đã công bố mười tiến bộ toán học đáng kinh ngạc trong một hơi thở.
Trong đó bao gồm:
- Lần đầu tiên chứng minh được sự tồn tại của nhóm phi Sofic (Non-sofic groups);
- Đưa ra giới hạn dưới mới cho mạch điện (Circuit lower bounds);
- Chinh phục giới hạn độ khó của bài toán Vector gần nhất (Closest Vector Problem, CVP);
- Và định lý lặp lại song song lượng tử cho trò chơi hai người (Quantum parallel repetition).
Điều khiến Phó giáo sư Henry Yuen tại Đại học Columbia bận tâm nhất là cái cuối cùng——
Năm 2016, Yuen đã đạt được tiến bộ quan trọng trên vấn đề này, nhưng chưa giải quyết triệt để. 10 năm qua, ông liên tục thất bại, thậm chí một tháng trước ông còn dùng ChatGPT 5.5 để một lần nữa tấn công vào chứng minh cuối cùng, nhưng thu được rất ít.
Và AI, trên vai ông, chỉ khẽ một cú đá, đưa quả bóng vào lưới.
Chứng minh đúng, nhưng con người không hiểu
Vài ngày trước, Lijie Chen đã gửi cho Henry Yuen và một vài người khác một bản thảo bài báo.
Lúc đó cuộc sống rất bận rộn, ông không có thời gian nghiên cứu sâu. Giờ đây, bài báo đã được công bố. Ông không thể không nói ra, có điều muốn nói.
Định lý lặp lại song song lượng tử (Quantum parallel repetition theorem), là lĩnh vực Henry Yuen đã dành nhiều năm tâm huyết nghiên cứu từ thời nghiên cứu sinh, và cũng là thành tựu ông tự hào nhất.
Henry Yuen, hiện là Phó giáo sư Khoa học Máy tính gia đình Srivani, Đại học Columbia
Ông nhớ những buổi chiều ngồi trong quán cà phê, những đêm khuya trong văn phòng, và vô số ngày cuối tuần đáng lẽ được nghỉ ngơi, liên tục mổ xẻ nghiên cứu định lý lặp lại song song kinh điển của Ran Raz.
Ông muốn giải quyết phiên bản lượng tử của định lý này, vì thế đêm không ngủ, trằn trọc. Ông đã tiếp thu hàng tấn công cụ toán học, và cuối cùng thành công chứng minh được sự suy giảm đa thức.
https://arxiv.org/pdf/1604.04340
Quan trọng hơn, ông đã xây dựng được niềm tin từ đó, cuối cùng nhận ra năng lực của bản thân, chứng minh rằng ông thực sự có thể giải quyết những vấn đề (ít nhất là một phần) mà người khác cũng quan tâm.
Ông tin rằng chứng minh này của OpenAI có lẽ là đúng, bởi đã có chứng minh hình thức hóa Lean. Nhưng để tiêu hóa chứng minh mới này, Henry Yuen vẫn cần một chút thời gian.
Mặc dù chứng minh mới thực sự tiếp tục từ nơi ông dừng lại trước đó, nhưng AI đã phá vỡ giới hạn chiến lược chứng minh ban đầu của ông, sử dụng một số kỹ thuật và phương pháp. Những phương pháp này có lẽ đã được các nhà nghiên cứu trong lĩnh vực lý thuyết toán tử (operator theory) và phân tích hàm (functional analysis) nắm vững.
Ngoài sự phấn khích, cảm nhận đầu tiên của Yuen là thất vọng, thất vọng về phong cách viết bài báo.
Ông nói chứng minh này đọc lên đầy mùi AI: phần dẫn nhập dài dòng vòng vo, nhưng các khâu then chốt lại như ảo thuật, khiến người ta hoang mang.
Chứng minh của OpenAI, đọc khá thú vị, nhưng cũng hơi đau đầu.
Nó đầu tiên đặt vấn đề ngay ngắn trên bàn, sau đó đột nhiên nhảy sang hướng 'dùng biểu thức giải (resolvent) để tìm sự tinh khiết (purification) đúng', giữa chừng hầu như không để lại bậc thang logic nào.
Tiếp theo, là một loạt tính toán entropy ma trận khá khác thường, tính toán quanh co, cuối cùng nói với bạn: con đường này đi được.
Nhưng bước then chốt nhất, trực giác đó đến từ đâu, nó không nói.
Và nét bút tinh tế nhất, đòi hỏi sáng tạo nhất——kỹ thuật mở rộng không gian toán tử bằng cách sử dụng phép biến đổi Uhlmann (Uhlmann transformation), lẽ ra phải là cao trào hào hứng nhất của toàn bộ chứng minh, lại bị AI vứt bỏ như bùn đất, bị ném vào Phần 4 mà không có cảnh báo, không có giải thích.
Chứng minh đúng, nhưng lại giấu đi ý tưởng quan trọng nhất.
Ông hy vọng OpenAI có thể dành thêm một vài từ khóa gợi ý (prompt), chỉnh sửa kỹ bài viết này.
Đau lòng hơn là tầng thứ hai: Lean xác minh thành công, không có nghĩa là hiểu.
Máy móc có thể đảm bảo mỗi bước suy luận không thể bắt bẻ, nhưng "tại sao chiêu này hiệu quả", "nó có ý nghĩa gì trong bản đồ lý thuyết rộng lớn hơn", "còn có thể dùng ở đâu"——những câu hỏi này, Lean không trả lời được cái nào.
Yuen thừa nhận, cho đến giờ ông vẫn đang tiêu hóa chứng minh này.
Đáp án đặt trước mặt, nhưng ông phải như đọc bài báo của người ngoại đạo, từng dòng một khôi phục lại trực giác mà AI không nói ra.
Đúng vậy, là có một chứng minh Lean ở đó. Nhưng đó chỉ là hình thức hóa, không có nghĩa là tôi hiểu. Thực sự muốn tiêu hóa, e rằng chỉ có thể dựa vào thời gian mài mòn từ từ.
Quả thực, AI đã mở rộng biên giới hiểu biết của con người, nhưng rồi sao? Niềm vui và ý nghĩa của nghiên cứu còn lại gì? Nếu AI giải quyết hết những vấn đề hóc búa mà ông hằng trăn trở, ông còn lại gì?
Câu hỏi tiếp nối nhau. Nhưng có một điều ông ngày càng xác định: những ngày sắp tới của các nhà toán học sẽ không nhàn rỗi, vừa phải thuần phục những con thú tư tưởng khổng lồ này, lại còn phải dịch ngôn ngữ "đen" của chúng ra tiếng người.
AI 'bác bỏ' giả thuyết toán học trăm năm bị phanh phui! Lean cũng không phải két sắt
Tuần trước, Ramana Kumar đã dùng 300 dòng Lean để bác bỏ giả thuyết toán học chưa giải nổi nổi tiếng nhất "Giả thuyết Collatz" (Collatz conjecture).
Nó hỏi một vấn đề đặc biệt đơn giản: cho bạn một số nguyên dương, thao tác lặp lại theo hai quy tắc——số chẵn thì chia cho 2, số lẻ thì nhân 3 cộng 1——cuối cùng có phải bất kể xuất phát từ số nào, đều sẽ rơi xuống 1?
Bạn có thể tính thử:
Giả thuyết này nói rằng: bất kể bạn lấy số nguyên dương nào bắt đầu, cuối cùng đều sẽ rơi vào vòng lặp 4→2→1 này.
Vấn đề này từ khi được nhà toán học Lothar Collatz đề xuất năm 1937, không ai có thể chứng minh nó đúng, cũng không tìm thấy phản ví dụ.
Nó được nhà toán học Paul Erdős gọi là: "Toán học chưa sẵn sàng ứng phó với vấn đề như vậy", còn Viện sĩ Viện Hàn lâm Khoa học Hoa Kỳ, nhà toán học Jeffrey Lagarias thì cho rằng "đây là một vấn đề cực kỳ khó, hoàn toàn vượt quá phạm vi toán học hiện nay".
Nếu bị bác bỏ, chắc chắn là tin tức gây chấn động giới toán học.
Đáng tiếc, 3 ngày sau, chứng minh hình thức hóa Lean này bị tuyên bố vô hiệu, bởi vì nó thực chất chỉ lợi dụng một lỗ hổng cấp thấp trong lõi của Lean.
Daniel Selsam của OpenAI, cùng một AI chuyên về an ninh mạng, đã hỗ trợ Lean FRO thực hiện một cuộc kiểm toán lõi.
Kết quả, họ phát hiện trong lõi Lean không chỉ một lỗ hổng!
Gần như cùng thời điểm, Giáo sư toán học Đại học Rutgers, cố vấn tổ chức nghiên cứu chuyên sâu Lean Alex Kontorovich đăng bài nhắc nhở: đừng coi Lean là người xác minh toàn năng.
Ông chỉ thẳng điểm chết——Sự căn chỉnh ngữ nghĩa (Semantic Alignment).
Ngay cả khi lõi Lean không thể bắt bẻ, Lean chỉ quản việc biên dịch mã. Ai đảm bảo "định nghĩa" bạn viết trong mã và "ý đồ trực giác" của con người trong ngôn ngữ tự nhiên là một chuyện?
Lean chỉ có thể xác nhận một việc: mã biên dịch thành công, logic hình thức không sai. Nhưng nó tuyệt đối không xác minh một vấn đề còn quan trọng hơn: lời phát biểu hình thức hóa này, có thực sự tương ứng với định lý bạn muốn chứng minh không?
Định lý chứng minh đúng, đề bài chép sai, Lean vẫn bật đèn xanh thông qua.
Và vấn đề căn chỉnh này, không thể hoàn toàn dựa vào máy tính giải quyết.
Trong bài phát biểu tại ICM 2026, Kontorovich đã chỉ ra: điểm mù lớn nhất của toán học hình thức hóa, không nằm ở "suy luận đúng", mà ở "nói đúng lời". Cuối cùng rà soát, vẫn phải là chuyên gia con người.
Lý do Liquid Tensor Experiment năm đó được tôn sùng, nhờ vào chính việc các nhà nghiên cứu kiểm tra thủ công từng định nghĩa toán học một cách gần như cưỡng chế.
Đặt lời của hai vị giáo sư lại với nhau, chỉ về cùng một sự thật: AI có thể chứng minh, máy móc có thể xác minh, nhưng việc hiểu và rà soát, vẫn là phần việc của con người.
Cuối cùng, còn có một tin đồn về mô hình lập luận AI:
Tài liệu tham khảo:
https://www.henryyuen.net/posts/on-openai-and-quantum-parallel-repetition/
https://x.com/AlexKontorovich/status/2083919186825236831
https://x.com/henryquantum/status/2083623700608237956
Bài viết từ tài khoản công chúng WeChat "Tân Trí Nguyên", tác giả: ASI Khải Thị Lục; biên tập: David
