OpenAI AI chứng minh các định lý toán học quan trọng, xác minh Lean gây tranh cãi

Mô hình suy luận mới nhất của OpenAI đã công bố mười tiến bộ toán học đáng kinh ngạc.

Bao gồm:

• Đã chứng minh lần đầu tiên sự tồn tại của các nhóm không Sofic (Non-sofic groups);
• Đã đưa ra các giới hạn mạch mới hoàn toàn (Circuit lower bounds);
• Đã vượt qua 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ử với suy giảm mũ (Quantum parallel repetition).

Điều khiến phó giáo sư Henry Yuen của Đại học Columbia quan tâm nhất là cái cuối cùng—

Năm 2016, Yuen đã đạt được tiến triển đáng kể về vấn đề này, nhưng chưa giải quyết triệt để. Trong 10 năm qua, anh ấy liên tục thất bại, thậm chí cách đây một tháng, anh ấy còn sử dụng ChatGPT 5.5 để lần nữa tấn công vào chứng minh cuối cùng, nhưng thu hoạch được rất ít.

Và AI, trên vai anh ta, nhẹ nhàng đá một chân, đưa bóng vào lưới.

Vài ngày trước, Lijie Chen đã gửi bản nháp bài báo cho Henry Yuen và một vài người khác.

Lúc đó cuộc sống rất bận rộn, anh ấy không có thời gian nghiên cứu sâu. Giờ đây, bài luận đã được công bố. Anh ấy cảm thấy phải nói ra những điều này.

Định lý lặp lại song song lượng tử (Quantum parallel repetition theorem) là lĩnh vực mà Henry Yuen đã dành nhiều năm nghiên cứu trong thời gian làm 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 họ Srivani tại Đại học Columbia

Anh ấy nhớ những buổi chiều ngâm mình trong quán cà phê, những đêm khuya ngồi trong văn phòng, và vô số những cuối tuần đáng ra nên nghỉ ngơi, lặp đi lặp lại việc phân tích và nghiên cứu định lý lặp song song kinh điển của Ran Raz.

Anh ấy muốn giải quyết phiên bản lượng tử của định lý này, đến nỗi không ngủ được, trằn trọc suốt đêm. Anh ấy đã tiêu thụ hàng tấn công cụ toán học và cuối cùng đã chứng minh thành công sự suy giảm đa thức.

https://arxiv.org/pdf/1604.04340

Quan trọng hơn, anh ấy đã xây dựng được sự tự tin, cuối cùng nhận ra năng lực thực sự của bản thân và chứng minh rằng anh ấy 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.

Anh ấy tin rằng bằng chứng của OpenAI nên là chính xác, bởi đã có chứng minh hình thức bằng Lean. Nhưng để hiểu rõ bằng chứng mới này, Henry Yuen vẫn cần thêm thời gian.

Mặc dù chứng minh mới thực sự tiếp tục từ nơi chứng minh trước đó kết thúc, nhưng AI đã vượt qua giới hạn của chiến lược chứng minh ban đầu, sử dụng một số kỹ thuật và phương pháp có thể đã được các nhà nghiên cứu trong lĩnh vực lý thuyết toán tử (operator theory) và giải tích hàm (functional analysis) nắm giữ.

Ngoài sự hưng phấn, cảm nhận đầu tiên của Yuen là sự thất vọng về phong cách viết luận văn.

Anh ấy nói bản chứng minh này đọc lên đầy mùi AI: phần mở đầu dài dòng, vòng vo mãi, nhưng các khâu then chốt lại như ảo thuật, khiến người đọc bối rối.

Bằng chứng từ OpenAI, khi đọc rất thú vị, nhưng cũng hơi khiến người ta đau đầu.

Nó trước tiên đặt vấn đề một cách rõ ràng lên bàn, rồi đột ngột nhảy sang hướng “sử dụng pre-solution để tìm purification đúng đắn”, gần như không có bất kỳ bước logic nào ở giữa.

Tiếp theo là một loạt phép tính entropy ma trận khá kỳ lạ, tính toán vòng vo rồi cuối cùng thông báo cho bạn: con đường này khả thi.

Nhưng bước quan trọng nhất, trực giác đó đến từ đâu, nó không nói rõ.

Và bước tinh vi nhất, đòi hỏi sự sáng tạo nhất — kỹ thuật sử dụng phép biến đổi Uhlmann để mở rộng không gian toán tử, vốn nên là cao trào đầy cảm xúc nhất của toàn bộ chứng minh, lại bị AI vứt bỏ như cát bụi, không báo trước, không giải thích, và bị ném vào phần thứ tư.

Bằng chứng đúng đắn, nhưng lại giấu đi ý tưởng quan trọng nhất.

Anh ấy mong OpenAI có thể dành thêm vài từ khóa để sắp xếp lại bản thảo này một cách chu đáo.

Điều khiến đau lòng hơn là cấp độ thứ hai: Việc Lean xác minh thành công không đồng nghĩa với việc hiểu rõ.

Máy móc có thể đảm bảo từng bước suy luận đều không thể chê vào đâu, nhưng những câu hỏi như “Tại sao mẹo này lại hiệu quả?”, “Nó có ý nghĩa gì trong bức tranh lý thuyết rộng lớn hơn?”, “Nó còn có thể được áp dụng ở đâu nữa?” — Lean không thể trả lời được bất kỳ câu nào trong số đó.

Yuen thừa nhận rằng anh ấy vẫn đang cố gắng thấm nhuần bằng chứng này.

Câu trả lời đang ở ngay trước mặt, nhưng anh ta lại phải đọc từng dòng như thể đang phân tích một bài luận của người ngoài ngành, để khôi phục lại trực giác mà AI chưa nói ra.

Đúng vậy, 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ự thấm nhuần, có lẽ chỉ có thể chờ thời gian dần dần ngấm dần.

Đúng vậy, AI đã mở rộng ranh giới hiểu biết của con người, nhưng sau đó thì 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 đề mà anh ta luôn day dứt, thì anh ta còn lại gì?

Các câu hỏi nối tiếp nhau kéo đến. Nhưng có một điều anh ấy ngày càng chắc chắn: những ngày tới của nhà toán học sẽ không hề nhàn rỗi—anh ấy phải thuần hóa những con quái vật tư tưởng này và dịch thuật ngôn ngữ chuyên ngành của chúng thành thứ dễ hiểu hơn.

Tuần trước, Ramana Kumar đã sử dụng 300 dòng Lean để bác bỏ bài toán chưa giải được nổi tiếng nhất — giả thuyết Collatz.

Câu hỏi của nó rất đơn giản: Cho một số nguyên dương, lặp lại thao tác theo hai quy tắc — nếu là số chẵn thì chia cho 2, nếu là số lẻ thì nhân với 3 rồi cộng thêm 1 — cuối cùng, liệu có đúng là bất kể bắt đầu từ số nào, bạn cũng sẽ luôn giảm xuống đến 1?

Bạn có thể tính toán:

Giả thuyết này nói rằng: bất kể bạn bắt đầu với số nguyên dương nào, cuối cùng bạn cũng sẽ rơi vào vòng lặp 4→2→1.

Kể từ khi nhà toán học Lothar Collatz đưa ra vào năm 1937, chưa ai có thể chứng minh nó đúng hoặc tìm ra 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 để đối mặt với những vấn đề như vậy”, trong khi nhà toán học Jeffrey Lagarias, thành viên của Học viện Khoa học Hoa Kỳ, cho rằng “Đây là một vấn đề cực kỳ khó khăn, hoàn toàn nằm ngoài phạm vi của toán học hiện đại”.

Nếu bị bác bỏ, đây chắc chắn sẽ là tin tức gây chấn động trong giới toán học.

Tiếc là, ba ngày sau, bản chứng minh Lean chính thức này bị tuyên bố vô hiệu vì thực chất nó chỉ khai thác một lỗ hổng hạ tầng trong lõi Lean.

Daniel Selsam từ OpenAI, cùng với một AI chuyên về an ninh mạng, đã hỗ trợ Lean FRO thực hiện cuộc kiểm toán lõi.

Kết quả, họ đã phát hiện không chỉ một lỗ hổng trong lõi Lean!

Gần như cùng thời điểm, giáo sư toán học tại Đại học Rutgers và cố vấn của tổ chức nghiên cứu Lean, Alex Kontorovich, đã đăng bài cảnh báo: Đừng coi Lean là người xác minh vạn năng.

Anh ấy trực tiếp chỉ vào điểm yếu——sự căn chỉnh ngữ nghĩa (Semantic Alignment).

Ngay cả khi lõi Lean hoàn hảo, Lean chỉ xử lý việc biên dịch mã. Ai sẽ đảm bảo rằng những gì bạn định nghĩa trong mã và ý định trực quan của con người trong ngôn ngữ tự nhiên là một điều giống nhau?

Điều duy nhất Lean có thể xác nhận là mã được biên dịch thành công và logic hình thức là chính xác. Nhưng nó hoàn toàn không xác minh một vấn đề quan trọng hơn nhiều: liệu lời phát biểu hình thức này có thực sự tương ứng với định lý bạn muốn chứng minh không?

Chứng minh định lý đúng, nhưng chép sai đề bài, Lean vẫn cho phép qua.

Tuy nhiên, vấn đề căn chỉnh này không thể giải quyết hoàn toàn bằng máy tính.

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 không nằm ở việc “suy luận đúng”, mà ở việc “nói đúng lời”. Người cuối cùng kiểm soát vẫn là các chuyên gia con người.

Lý do Liquid Tensor Experiment trở nên huyền thoại chính là nhờ các nhà nghiên cứu thực hiện việc kiểm tra thủ công gần như điên cuồng đối với từng định nghĩa toán học.

Khi xem xét lời của hai giáo sư cùng nhau, chúng đều chỉ ra một sự thật: AI có thể chứng minh, máy móc có thể xác minh, nhưng sự hiểu biết và kiểm soát vẫn là công việc của con người.

Cuối cùng, còn một tin đồn về mô hình suy 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 này đến từ tài khoản WeChat “New Intelligence Yuan”, tác giả: Revelation of ASI; biên tập: David