Mục lục
TL;DR: OpenAI đã đưa lên GitHub 372 phép chứng minh trong toán học thuần túy, trong đó có kết quả liên quan tới 23 bài toán Erdős, nhưng các chứng minh này vẫn cần được chuyên gia đọc, kiểm tra và xác nhận độc lập.
Theo Thomas Bloom, người vận hành Erdosproblems.com, cả 23 kết quả liên quan đến cơ sở dữ liệu bài toán Erdős đều đáng chú ý và có ý nghĩa. Đợt công bố ngày 6/10 gồm tổng cộng 1.268 trang bài viết, trung bình khoảng 55 trang cho mỗi bài toán trong nhóm này.
Quy mô của đợt phát hành khiến đây trở thành một bước đi lớn trong nỗ lực dùng AI cho nghiên cứu toán học. Tuy vậy, Bloom nhấn mạnh bài tổng hợp của ông chỉ liệt kê các tuyên bố, không phải sự chứng thực rằng chúng đúng hoặc đã giải quyết dứt điểm các bài toán cho cộng đồng toán học.
23 bài toán và các tuyên bố nổi bật
Danh sách gồm các bài toán mang số 3, 90, 120, 138, 148, 172, 181, 184, 293, 304, 371, 416, 431, 508, 551, 604, 802, 821, 952, 968, 970, 1083 và 1150 trong cơ sở dữ liệu Erdős. Có 12 bài nằm trong danh sách FrontierMath Erdős, một tập bài toán thường được theo dõi như thước đo năng lực AI làm toán, trong đó bài 508 mới được tính một phần.
Với bài 3 về cấp số cộng, OpenAI tuyên bố có một cận dạng gần đa thức cho định lý Szemerédi ở mọi độ dài cấp số cộng. Nếu đúng, kết quả này sẽ kéo theo một phỏng đoán nổi tiếng của Erdős: một tập số nguyên có tổng nghịch đảo phân kỳ sẽ chứa các cấp số cộng dài tùy ý. Bài viết đi kèm cho kết quả này dài 198 trang; Bloom lưu ý tệp Lean hiện chỉ chứng minh một cận yếu hơn.
Ở bài 90 về khoảng cách đơn vị, tuyên bố mới đưa ra cận trên rằng n điểm trên mặt phẳng tạo ra nhiều nhất n^(4/3−c) cặp điểm cách nhau một đơn vị. Đây sẽ là cải thiện so với cận n^(4/3) tồn tại lâu nay, dù tài liệu không nêu giá trị của c. Với bài 508, nhóm tác giả tuyên bố mọi cách tô 5 màu mặt phẳng đều có hai điểm cùng màu cách nhau một đơn vị, hàm ý số màu sắc của mặt phẳng là 6 hoặc 7.
Các điểm đáng chú ý khác gồm cận O(2^n) cho số Ramsey của hypercube n chiều ở bài 181; khả năng tách mọi đồ thị n đỉnh thành O(n) chu trình và cạnh rời nhau ở bài 184; và cận dưới xác nhận phỏng đoán Erdős về số van der Waerden hai màu ở bài 138. Bài 431 được mô tả là chứng minh phỏng đoán Ostmann, còn gọi là bài toán Goldbach ngược.
Formal hóa Lean có mặt ở 19 kết quả
19 trong 23 kết quả đi kèm formal hóa bằng Lean, một hệ thống trợ lý chứng minh cho phép máy kiểm tra các bước suy luận theo ngôn ngữ hình thức. Bốn bài chưa có formal hóa Lean là 172, 181, 821 và 1083.
Tuy nhiên, việc có tệp Lean không đồng nghĩa kết quả đã được xác nhận hoàn toàn. Bloom nói ông chưa kiểm tra liệu các formal hóa có biên dịch thành công hay không, cũng chưa đối chiếu xem phát biểu hình thức có phản ánh chính xác bài toán gốc hay không.
Trong các tuyên bố khác, bài 172 liên quan đến phỏng đoán Hindman về tổng và tích của các tập số cùng màu; bài 1083 nói rằng n điểm trong không gian d chiều xác định ít nhất n^(2/d) khoảng cách khác nhau. Bloom nhận xét kết quả ở bài 1083, nếu đúng như nêu, mạnh hơn cả phỏng đoán ban đầu của Erdős.
Khâu kiểm chứng vẫn mới bắt đầu
Bloom cho biết ông chưa xem xét nghiêm túc từng chứng minh. Ông đánh giá các bài viết được trình bày kém theo kiểu thường thấy ở đầu ra AI; trong các tác vụ cần diễn giải, cách đặt bối cảnh cho prompt có thể ảnh hưởng đáng kể đến mức độ rõ ràng của câu trả lời. Dù vậy, ông cho rằng chúng có thể là nguồn nguyên liệu phong phú để các nhà toán học rút gọn, kiểm tra và diễn giải lại.
Vì thế, 23 bài toán chưa nên được xem là đã khép lại đối với giới nghiên cứu. Ngoài việc xác minh tính đúng đắn, các chuyên gia còn phải đánh giá tính mới, làm rõ lập luận và xác định liệu có những cách tiếp cận của con người khác với hướng đi của AI hay không.
Tranh luận về cách công bố cũng đã xuất hiện. Terence Tao từng chỉ trích việc tung nhiều chứng minh cùng lúc vì có thể làm giảm khả năng cộng đồng toán học tiêu hóa và phát triển các ý tưởng. Một nhóm nhà toán học mới cũng cáo buộc OpenAI không tuân thủ các chuẩn mực nghiên cứu khoa học. Theo thông tin được nêu, OpenAI nói họ đã tham vấn nhóm cố vấn về toán học và AI của Institute for Advanced Study trước khi quyết định chia sẻ kết quả.
Vì sao đáng chú ý?
Đợt công bố diễn ra sau một giai đoạn nhiều tín hiệu trái chiều về AI giải toán. Tháng 10/2025, các tuyên bố GPT-5 giải được 10 bài Erdős đã bị bác bỏ vì phần lớn là tìm lại lời giải có sẵn trong tài liệu. Đến tháng 1/2026, GPT-5.2 Pro tạo ra lời giải gần như tự chủ cho bài 728 cùng một số bài khác, dù một kết quả sau đó bị phân loại lại khi phát hiện lời giải trước đó đã tồn tại.
Ngày 20/5, OpenAI thông báo một mô hình suy luận đa dụng đã bác bỏ phỏng đoán năm 1946 của Erdős về bài toán khoảng cách đơn vị trên mặt phẳng, thuộc bài 90. Kết quả tháng 5 là cận dưới, còn tuyên bố mới hướng tới cải thiện cận trên của cùng bài toán. Nếu các chứng minh lần này được xác nhận, chúng có thể cho thấy AI đang mở rộng từ các bài dễ tiếp cận sang những câu hỏi nổi bật hơn trong tổ hợp, lý thuyết số và hình học. Nhưng ở thời điểm hiện tại, giá trị khoa học của chúng vẫn phụ thuộc vào quá trình kiểm chứng kéo dài của con người.
Skills Bridge tổng hợp
