Ngày 1/8/2026, OpenAI công bố rằng một phiên bản nội bộ của Astra — mô hình lớn thế hệ tiếp theo của hãng, hiện chưa phát hành — đã tạo ra kết quả mới cho 10 bài toán mở trong toán học và khoa học máy tính lý thuyết. Mỗi bài toán này đều đã "treo" (chưa ai giải được) ít nhất một thập kỷ, nhiều bài lâu hơn nhiều. Nhưng điểm khiến giới chuyên môn chú ý không chỉ là các lời giải, mà là cách chúng có thể được kiểm chứng.
Chuyện gì đã xảy ra
OpenAI đăng kèm một bộ tài liệu dài 249 trang, phần "tường thuật" quá trình suy luận của mô hình, và — quan trọng nhất — chứng chỉ Lean 4 (Lean certificate) cho cả 10 kết quả, đưa lên một kho GitHub công khai. Việc công bố này cũng chính là lần đầu OpenAI chính thức giới thiệu tên mô hình Astra.
Kết quả nổi bật nhất là lần đầu tiên dựng được một "nhóm non-sofic" — trả lời một câu hỏi trung tâm của lý thuyết nhóm, tồn tại từ khi nhà toán học Mikhail Gromov nêu khái niệm "soficity" vào năm 1999. Suốt 27 năm, không nhà toán học nào chứng minh hay bác bỏ được; Astra đưa ra ví dụ cho thấy: không, không phải nhóm nào cũng sofic.
Chín kết quả còn lại trải rộng nhiều lĩnh vực, trong đó có: bác bỏ giả thuyết rigidity của Connes (do nhà toán học đoạt giải Fields Alain Connes nêu năm 1980), chứng minh giả thuyết thể tích Ehrhart, giải ba bài toán trong danh mục nổi tiếng của Erdős, và cải thiện lần đầu tiên kể từ 1978 về chặn trên cho bài toán xếp cầu trong không gian nhiều chiều.
Vì sao đây là tin lớn — điểm mấu chốt là "kiểm chứng được"
Chuyện AI "làm toán" không mới. Điều khiến lần này khác hẳn là phần hình thức hoá bằng Lean 4.
Nói đơn giản: Lean là một hệ thống mà trong đó mọi bước của một chứng minh phải được máy kiểm tra đến tận gốc dựa trên các tiên đề toán học. Kết quả chỉ có hai khả năng: chứng chỉ hoặc "biên dịch" trọn vẹn (đúng), hoặc thất bại (sai) — không có vùng xám. Vì OpenAI đã đưa cả 10 chứng chỉ lên GitHub công khai, bất kỳ ai cài trình biên dịch Lean đều có thể tự kiểm chứng từng lời giải, mà không cần tin lời OpenAI, không cần chờ nhiều tháng bình duyệt như thông lệ. Theo mô tả, kho mã báo "sorry count = 0" — tức không có bước nào trong các chứng minh bị bỏ ngỏ.
Đây chính là bước chuyển đáng chú ý: từ chỗ AI "đưa ra câu trả lời, con người phải tin và kiểm tra thủ công", sang AI đưa ra câu trả lời kèm bằng chứng mà máy có thể tự kiểm trong vài phút.
Chi phí và cách làm
Theo OpenAI, tổng lượng tính toán để tìm ra lời giải cho cả 10 bài chỉ tốn khoảng 2.000 USD tính theo giá API hiện hành. Quy trình: mô hình tạo ra các lập luận; con người dùng chính mô hình đó biên tập thành bản thảo; rồi mô hình hình thức hoá từng lập luận thành chứng chỉ Lean. Kết quả được công bố bởi nhà nghiên cứu Sébastien Bubeck của OpenAI; đây cũng là dòng mô hình từng xử lý một giả thuyết của Erdős hồi tháng 5.
Cần nhìn tỉnh táo: vài điểm còn tranh luận
Đây là công bố của chính OpenAI, nên cũng cần đọc với sự cân nhắc:
- Astra chưa phát hành. Đây là phiên bản nội bộ; công chúng chưa dùng được, và (theo một số nguồn) mô hình còn phải qua vòng đánh giá an toàn trước khi ra mắt.
- Một số nhà phê bình đặt câu hỏi về cách chọn bài toán và việc bên ngoài không được truy cập mô hình để tự kiểm tra khả năng — nghĩa là khó lặp lại độc lập kết quả bằng chính mô hình đó.
- Tuy vậy, điểm mạnh khó bác bỏ là: bản thân các lời giải thì kiểm chứng được nhờ Lean, độc lập với việc bạn có tin OpenAI hay không.
Điều này có ý nghĩa gì với người đọc
Với đa số chúng ta — không làm toán lý thuyết — giá trị của tin này không nằm ở các bài toán, mà ở hai xu hướng nó cho thấy:
- AI đang tiến từ "trợ lý" sang "tạo ra tri thức mới có thể kiểm chứng". Ngưỡng năng lực của các mô hình frontier tiếp tục dịch lên, nhanh hơn nhiều người hình dung.
- Mô hình "đưa ra kết quả kèm bằng chứng tự kiểm" là một hướng đi cho AI đáng tin. Trong công việc, đây là bài học đáng suy ngẫm: thay vì hỏi "AI trả lời có đúng không rồi tin", ta nên ưu tiên những cách dùng mà kết quả của AI có thể được đối chiếu, kiểm tra lại bằng nguồn hoặc dữ kiện độc lập — đúng tinh thần "không tin ngay, luôn kiểm chứng" mà chúng ta vẫn theo.
Astra sẽ ra mắt chính thức khi nào, mạnh tới đâu trong các tác vụ đời thường, vẫn còn ở phía trước. Nhưng cách OpenAI công bố lần này — kèm bằng chứng ai cũng kiểm được — có lẽ là phần đáng học nhất của câu chuyện.
References
- OpenAI — Ten advances in mathematics and theoretical computer science. Available at: https://openai.com/index/ten-advances-in-mathematics/ (Accessed: 04/08/2026).
- SiliconANGLE — OpenAI's Astra solves 10 long-open math problems and publishes the proofs. Available at: https://siliconangle.com/2026/08/02/openais-astra-solves-10-long-open-math-problems-publishes-proofs/ (Accessed: 04/08/2026).
- The Next Web — OpenAI says its next model, Astra, has solved ten open problems in mathematics. Available at: https://thenextweb.com/news/openai-astra-model-ten-math-proofs-non-sofic-groups (Accessed: 04/08/2026).
- Forbes — OpenAI's Astra Solved 10 Decades-Old Math Problems For Just $2,000. Available at: https://www.forbes.com/sites/jonmarkman/2026/08/03/openais-astra-solved-10-decades-old-math-problems-for-just-2000/ (Accessed: 04/08/2026).
- TechTimes — OpenAI's Astra Solves Ten Decade-Old Math Problems With Machine-Checkable Lean Proofs. Available at: https://www.techtimes.com/articles/322710/20260802/openais-astra-solves-ten-decade-old-math-problems-machine-checkable-lean-proofs.htm (Accessed: 04/08/2026).
- Pondero — OpenAI reveals Astra through ten machine-verified open-problem proofs. Available at: https://pondero.ai/news/2026-08-02-openai-astra-math-proofs/ (Accessed: 04/08/2026).