Mô hình AI Trung Quốc hỗ trợ chứng minh giả thuyết Ghys trong không gian ba chiều, Lean kiểm chứng toán học

Một bài toán toán học từ năm 1995 đạt cột mốc mới

Một giả thuyết toán học được nêu ra năm 1995 đã có lời giải trong trường hợp số chiều phức bằng ba, nhờ sự hợp tác giữa các nhà toán học và mô hình Intern-S2 của Phòng thí nghiệm AI Thượng Hải. Sau đó, một nhóm tại Đại học Bắc Kinh chuyển bốn định lý chính của bài báo thành các chứng minh được Lean kiểm tra, một hệ thống máy tính được thiết kế để xác minh lập luận toán học.

Phòng thí nghiệm AI Thượng Hải công bố thành tựu ngày 15 tháng 10 năm 2026, ghi nhận đóng góp của nhóm do Disheng Xu dẫn dắt. Ông là giáo sư tại Đại học Great Bay và học giả thỉnh giảng tại phòng thí nghiệm. Bài nghiên cứu mang tên Codimension-one holomorphic Anosov diffeomorphisms ghi Jiesong Zhang, thuộc Viện Công nghệ Hoàng gia KTH của Thụy Điển, là tác giả duy nhất.

Kết quả giải quyết trường hợp đối chiều một của giả thuyết do nhà toán học Pháp Etienne Ghys đề xuất, bao gồm trường hợp số chiều phức bằng ba. Giả thuyết đề cập đến mối liên hệ đáng chú ý giữa chuyển động và hình dạng: liệu một không gian có hỗ trợ một dạng chuyển động hỗn loạn nhất định thì bản thân nó có phải mang cấu trúc toán học có trật tự cao hay không.

Intern-S2 hỗ trợ phát triển ý tưởng và lập luận thông qua nhiều vòng trao đổi với các nhà nghiên cứu. Trong tuyên bố về việc sử dụng AI, Zhang cho biết ông đã tự mình kiểm chứng toàn bộ phần toán học. Sự hợp tác kết hợp khả năng khám phá của máy, phán đoán của con người và một quy trình kiểm chứng hình thức độc lập.

Phòng thí nghiệm mô tả đây là lần đầu một mô hình AI Trung Quốc hỗ trợ giải quyết một bài toán toán học có tầm vóc như vậy. Kết quả cụ thể là một định lý phân loại, đi kèm bản thảo tiền xuất bản công khai và mã hình thức hóa được phát hành rộng rãi.

Chứng minh cho biết gì về chuyển động và hình dạng

Giả thuyết Ghys thuộc lĩnh vực động lực học phức, nghiên cứu sự thay đổi của các hệ toán học khi tọa độ của chúng tuân theo quy tắc của số phức. Một số phức có hai thành phần thực, vì vậy số chiều phức bằng ba tương ứng với sáu chiều thực trong lân cận. Bối cảnh này trừu tượng hơn nhiều so với một vật thể thông thường chuyển động trong phòng.

Hệ Anosov có sự kết hợp chính xác giữa kéo giãn và co nén. Qua chuyển động lặp đi lặp lại, một số phương có thể co lại trong khi những phương khác giãn ra. Các điểm xuất phát gần nhau có thể nhanh chóng tách xa, tạo nên hành vi hỗn loạn dù quy tắc chi phối từng bước vẫn hoàn toàn xác định.

Có thể hình dung đó là một quá trình lặp đi lặp lại, kéo giãn rồi gấp một hình dạng. Hệ toán học được nghiên cứu ở đây có các điều kiện chặt chẽ hơn nhiều: sự giãn và co phải thỏa mãn những điều kiện đồng đều, còn chuyển động phải bảo toàn cấu trúc do các tọa độ phức tạo nên.

Ghys giả thuyết rằng những hệ như vậy trên các đa tạp phức compact phải có một mô tả đại số chuẩn tắc. Đa tạp là không gian trông đơn giản trong một vùng lân cận nhỏ, dù hình dạng tổng thể có thể phức tạp. Trong bối cảnh này, tính compact là điều kiện toán học giúp không gian không kéo dài vô hạn.

Định lý của Zhang cho biết mọi vi phôi Anosov chỉnh hình đối chiều một trên một đa tạp phức liên thông compact đều liên hợp song chỉnh hình với một tự đẳng cấu hyperbolic của một hình xuyến phức. Nói đơn giản hơn, một phép đổi tọa độ khả nghịch bảo toàn cấu trúc phức biến chuyển động đó thành một phép biến đổi đại số chuẩn tắc trên một không gian rất đều đặn.

Có thể xây dựng hình xuyến phức bằng cách đồng nhất các điểm trong không gian phức nếu chúng sai khác nhau bởi các phần tử của một mạng lặp lại. Thành tựu cốt lõi là động lực học phức tạp buộc không gian phải có mô tả hình học ngăn nắp này.

Vì sao phạm vi cụ thể rất quan trọng

Bài báo nghiên cứu trường hợp đối chiều một. Với các hệ này, điều đó có nghĩa là một trong hai phần co hoặc giãn có số chiều phức bằng một. Định lý áp dụng cho toàn bộ họ hệ bị giới hạn này và giải quyết giả thuyết trong trường hợp số chiều phức bằng ba.

Giả thuyết rộng hơn của Ghys đề cập đến các hệ Anosov chỉnh hình trên nhiều loại đa tạp phức hơn, đồng thời mô tả chúng bằng những mô hình đại số chuẩn tắc trên các không gian gọi là đa tạp infra-nil phức. Kết quả của Zhang đưa ra lời giải đặc biệt cứng nhắc cho trường hợp được nghiên cứu: một hình xuyến phức và một tự đẳng cấu hyperbolic.

Với các nhà toán học nghiên cứu trường hợp này, định lý chuyển trọng tâm từ việc xác định một không gian và chuyển động chưa biết sang nghiên cứu một mô hình chuẩn tắc. Phép đổi tọa độ liên kết hệ ban đầu với mô hình đó mà vẫn bảo toàn hình học phức.

Xu đã dành nhiều năm nghiên cứu bài toán này. Trước đó, ông cùng người hướng dẫn cũ là Artur Avila, chủ nhân Huy chương Fields, nghiên cứu trường hợp số chiều ba. Sau này, Xu và Zhang đạt được một số kết quả liên quan từng phần, được công bố trên Journal of the European Mathematical Society. Công trình mới là thành quả của quá trình theo đuổi bền bỉ cùng một câu hỏi toán học.

Từ bài kiểm tra Olympic đến quan hệ hợp tác nghiên cứu

Vai trò của Intern-S2 tiếp nối một kết quả trước đó của Intern-S1 tại Olympic Toán học Trung Quốc năm 2025. Năm đó, ủy ban của Hội Toán học Trung Quốc phụ trách các cuộc thi toán trung học tổ chức một bài kiểm tra AI, mời ba mô hình Trung Quốc giải bài trong cùng thời gian giới hạn như các thí sinh.

Intern-S1 đạt 102 điểm theo cùng thang chấm, đứng đầu trong ba mô hình tham dự. Ngưỡng huy chương vàng là 78 điểm, tức điểm số của mô hình cao hơn ngưỡng 24 điểm, tương đương khoảng 31%.

Xu nhận thấy dòng mô hình này có tiềm năng ứng dụng trong toán học nghiên cứu, còn Phòng thí nghiệm AI Thượng Hải muốn chuyển từ các bài toán thi đấu sang những câu hỏi chưa có lời giải. Hai bên bắt đầu hợp tác đầu năm 2026, trong đó có việc xây dựng một hệ thống phần mềm, được mô tả là Harness, để điều phối hoạt động của mô hình và các cuộc trao đổi với nhà nghiên cứu.

Các mốc chính gồm:

• 1995: Etienne Ghys đề xuất giả thuyết.
• 2025: Intern-S1 đạt 102 điểm trong bài kiểm tra AI của Olympic Toán học Trung Quốc.
• Đầu năm 2026: Xu và Phòng thí nghiệm AI Thượng Hải bắt đầu hợp tác huấn luyện mô hình.
• Tháng 3 năm 2026: Xu trở thành học giả thỉnh giảng tại phòng thí nghiệm.
• Tháng 8 năm 2026: Phiên bản Intern-S2 được phát triển nội bộ cùng hệ thống hỗ trợ đạt giai đoạn dùng cho hoạt động khám phá toán học chuyên sâu.
• Ngày 29 tháng 9: Bài báo của Zhang được đăng trên arXiv, sau đó cập nhật phiên bản mới ngày 13 tháng 10.
• Ngày 15 tháng 10 năm 2026: Thành tựu được công bố rộng rãi.

Các nhà toán học định hướng AI như thế nào

Trong lần đầu khám phá bài toán, Intern-S2 tạo ra một báo cáo suy luận dài khoảng 400 trang. Xu mời Zhang, học trò cũ của ông và là nhà nghiên cứu sau tiến sĩ tại KTH, tham gia với tư cách học giả thỉnh giảng. Zhang đã theo dõi giả thuyết Ghys từ khi làm nghiên cứu sinh.

Xu và Zhang xem xét các đề xuất của mô hình, xác định những hướng có triển vọng và đưa ra phản hồi để định hướng các lượt khám phá tiếp theo. Máy theo đuổi nhiều nhánh lập luận và tạo ra các luận cứ; các nhà toán học quyết định hướng nào đáng được nghiên cứu thêm và hỗ trợ hoàn thiện chứng minh cuối cùng.

Phòng thí nghiệm cho biết quá trình này gồm bảy đợt suy luận liên tiếp. Trong quá trình đó, đồ thị bài toán của mô hình mở rộng từ 15 nút lên 389 nút, còn lượng đầu ra tích lũy đạt khoảng một nghìn trang và gồm hàng chục hướng tiếp cận được đề xuất.

Đồ thị bài toán là bản đồ thể hiện các nhiệm vụ toán học nhỏ hơn và mối liên hệ giữa chúng. Một nút có thể biểu diễn một khẳng định trung gian, còn nút khác là kết quả cần có để chứng minh khẳng định đó. Mức tăng được báo cáo cho thấy hệ thống đã chia nhỏ và khám phá bài toán trên phạm vi rộng đến đâu.

Tuyên bố về việc sử dụng AI của Zhang nói rõ ai chịu trách nhiệm về phần toán học hoàn chỉnh: một phiên bản nội bộ của Intern-S2 hỗ trợ phát triển ý tưởng và lập luận qua nhiều vòng đối thoại, còn ông tự mình kiểm chứng phần toán học. Bài báo cũng cảm ơn Xu vì những cuộc trao đổi liên tục.

Phần mềm hỗ trợ đóng góp như thế nào

Phòng thí nghiệm AI Thượng Hải kết hợp mô hình với phần mềm được thiết kế để quản lý các chuỗi suy luận dài và những vòng phản hồi lặp lại từ con người. Hệ thống có thể chia một câu hỏi khó thành các nhiệm vụ nhỏ hơn, khám phá nhiều hướng và trả kết quả để nhà nghiên cứu đánh giá.

Phương pháp huấn luyện kết hợp kiến thức khoa học rộng với tài liệu hướng đến toán học nghiên cứu, trong đó có các bài toán khó lấy từ các công trình toán học và phương pháp kiểm tra lời giải được đề xuất. Phòng thí nghiệm cũng mô tả việc sử dụng học tăng cường với phần thưởng có thể kiểm chứng, nghĩa là những lập luận thành công và kiểm tra được có thể trở thành tín hiệu huấn luyện.

Sau đó, các nhà nghiên cứu dùng kinh nghiệm từ hệ thống hỗ trợ để cải thiện chính mô hình. Mục tiêu thực tiễn là duy trì tiến triển hữu ích trong suốt một cuộc khảo cứu dài, bao gồm theo dõi kết quả trung gian và sửa lỗi khi các lập luận mới được phát triển.

Phòng thí nghiệm cũng viện dẫn kết quả trên IMO-Proof và AdvancedMathBench, các bộ đánh giá tập trung vào suy luận toán học. Trong dự án Ghys, bằng chứng chi tiết nhất về cách hệ thống vận hành là chuỗi suy luận dài, phản hồi từ chuyên gia, bài báo hoàn chỉnh và quá trình kiểm chứng hình thức sau đó.

Đại học Bắc Kinh kiểm tra chứng minh ra sao

Nhóm của Đại học Bắc Kinh do Bin Dong và Ruochuan Liu dẫn dắt, sử dụng khuôn khổ SHEAF để hình thức hóa cả bốn định lý chính trong bài báo của Zhang. Công việc cũng bao gồm các kết quả của Ghys làm cơ sở cho những lập luận này.

Hình thức hóa là chuyển các định nghĩa, giả thiết và lập luận toán học sang một ngôn ngữ để máy tính có thể kiểm tra. Một bài báo thông thường có thể dựa vào độc giả được đào tạo để tự điền vào những bước quen thuộc. Lean đòi hỏi các bước đó phải được diễn đạt bằng những mệnh đề chính xác và các phép suy luận logic được cho phép.

Hai thành viên nhóm Jiedong Jiang và Bin Wu cho biết công việc mất khoảng năm ngày, với tối đa 100 tác nhân AI hoạt động song song. Kết quả là khoảng 550.000 dòng mã Lean. Các chuyên gia cũng kiểm tra để bảo đảm những mệnh đề hình thức phù hợp với ý nghĩa toán học của các định lý chính trong bài báo.

SHEAF tổ chức công việc thành một đồ thị có hướng gồm các định nghĩa, mệnh đề và quan hệ phụ thuộc. Nhờ đó, các tác nhân khác nhau có thể xử lý những phần liên kết với nhau, trong khi nhóm theo dõi được mệnh đề nào đã có chứng minh và mệnh đề nào còn cần giải quyết.

Việc hình thức hóa không chỉ là chuyển các lập luận cuối cùng sang ngôn ngữ máy. Một số kết quả hỗ trợ trong động lực học chưa có trong các thư viện toán học hình thức hiện có. Nhóm phải bổ sung phần nền tảng đó hoặc tìm cách sử dụng các kết quả sẵn có, rồi nối các phần thành một chuỗi hoàn chỉnh.

Bài báo có dưới dạng bản thảo tiền xuất bản trên arXiv, còn mã hình thức hóa đã được phát hành trên GitHub. Thông báo không nêu việc bài báo đã được đăng trên tạp chí hay có quyết định bình duyệt hay chưa.

Vì sao cần kết hợp hai giai đoạn

Intern-S2 và SHEAF đảm nhiệm những vai trò khác nhau. Công cụ thứ nhất hỗ trợ tìm kiếm ý tưởng và lập luận toán học. Công cụ thứ hai hỗ trợ xây dựng các chứng minh hình thức để Lean kiểm tra. Các nhà toán học hướng dẫn quá trình khám phá, kiểm tra phần toán học thu được và đánh giá xem các mệnh đề hình thức có diễn đạt đúng những định lý dự kiến hay không.

Quy mô công việc cho thấy rõ sự phân chia này. Khoảng một nghìn trang đầu ra thăm dò được dùng để xây dựng bài báo nghiên cứu; sau đó, quy trình kiểm chứng tạo ra khoảng 550.000 dòng mã hình thức. Mỗi giai đoạn chuyển công việc sang một dạng khác phù hợp với nhiệm vụ riêng.

Với các nhà nghiên cứu sau này, bài báo công khai trình bày lập luận toán học, còn mã công khai ghi lại cấu trúc chứng minh hình thức. Các định nghĩa và kết quả hỗ trợ được bổ sung trong quá trình hình thức hóa cũng có thể làm nền tảng cho những nghiên cứu tiếp theo trong cùng lĩnh vực.

Bước tiếp theo là một mô-đun kiểm chứng có thể tái sử dụng

Phòng thí nghiệm AI Thượng Hải dự định đóng gói quy trình này thành một mô-đun kiểm chứng toán học cho nền tảng khám phá khoa học Intern Duanyan. Mục tiêu là để các dự án sau có thể tái sử dụng sự kết hợp giữa hoạt động khám phá của mô hình, phản hồi từ chuyên gia và kiểm tra hình thức.

Phòng thí nghiệm cũng dự định áp dụng năng lực suy luận được phát triển trong dự án này vào những ngành khác có cấu trúc toán học liên quan. Quy trình dự kiến là giải một bài toán nghiên cứu, chuyển các phương pháp hữu ích thành phần mềm có thể tái sử dụng rồi áp dụng vào một nghiên cứu khác.

Với Xu, kết quả này tiếp nối mối quan tâm nghiên cứu lâu năm thông qua sự hợp tác giữa Đại học Great Bay, Phòng thí nghiệm AI Thượng Hải, KTH và Đại học Bắc Kinh. Với cộng đồng toán học rộng lớn hơn, công trình vừa đưa ra một kết quả phân loại mới, vừa cung cấp ví dụ chi tiết về việc AI tham gia nghiên cứu dưới sự định hướng của con người.

Điểm chính

• Chứng minh mới giải quyết trường hợp đối chiều một của giả thuyết Ghys, bao gồm số chiều phức bằng ba.
• Jiesong Zhang là tác giả duy nhất của bài nghiên cứu và cho biết ông đã tự mình kiểm chứng toàn bộ phần toán học.
• Disheng Xu và Zhang hướng dẫn Intern-S2 qua nhiều vòng khám phá và phản hồi.
• Đồ thị bài toán của mô hình tăng từ 15 nút lên 389 nút, cùng khoảng một nghìn trang suy luận.
• Khuôn khổ SHEAF của Đại học Bắc Kinh hỗ trợ hình thức hóa bốn định lý chính và các kết quả bổ trợ trong Lean.
• Quá trình kiểm chứng được cho là mất khoảng năm ngày và tạo ra khoảng 550.000 dòng mã.
• Phòng thí nghiệm dự định chuyển quy trình này thành một mô-đun kiểm chứng toán học có thể tái sử dụng.