OpenAI cho biết Astra, mô hình nội bộ thế hệ mới chưa ra mắt, đã đưa ra lời giải cho 10 bài toán mở trong toán học và tin học lý thuyết vốn chưa được giải suốt ít nhất một thập kỷ. Công ty đồng thời công bố các bản chứng minh hình thức có thể kiểm chứng bằng máy.

Theo SiliconANGLE và một số hãng tin quốc tế, ngày 2/8 theo giờ địa phương, OpenAI đã đăng lên GitHub một bản thảo dài 249 trang, lộ trình suy luận do mô hình tạo ra và bộ chứng chỉ Lean theo giấy phép Apache 2.0. OpenAI cho biết trong kho chứng chỉ được công bố, số mục “sorry” là 0, tức không còn bước nào bị bỏ dở trong các chứng minh hình thức.

Một trong những kết quả đáng chú ý nhất là lời giải cho bài toán xây dựng tường minh một nhóm phi-sofic, vấn đề còn bỏ ngỏ kể từ khi Mikhail Gromov đưa ra khái niệm sofic vào năm 1999. Astra cũng tạo ra phản ví dụ đối với giả thuyết về tính cứng do Alain Connes đề xuất năm 1980, đồng thời xây dựng được vô hạn nhóm có tính chất (T) khác nhau nhưng cùng chia sẻ một đại số von Neumann.

OpenAI cho biết Astra còn chứng minh được giả thuyết thể tích của Ehrhardt và giải thêm 3 bài trong danh sách các vấn đề của Paul Erdős, trong đó có bài số 183 liên quan đến số Ramsey nhiều màu.

Nhóm sofic là nhóm có thể được xấp xỉ bằng các hoán vị hữu hạn. Cho tới nay, mọi nhóm từng được nghiên cứu đều được xác nhận là sofic, trong khi mệnh đề “mọi nhóm đều là sofic” vẫn chưa được chứng minh. Theo OpenAI, Astra đã chỉ ra một ngoại lệ cho hướng hiểu phổ biến này.

Với giả thuyết của Connes, OpenAI diễn giải rằng thay vì tồn tại một “dấu vân tay” đủ để nhận diện duy nhất một nhóm trong một lớp nhóm cứng nhất định, Astra đã xây dựng được vô hạn nhóm khác nhau nhưng có cùng “dấu vân tay”.

Các kết quả còn lại trải rộng ở nhiều lĩnh vực như cấu hình khối cầu trong không gian nhiều chiều, mã nhị phân và mã cầu, độ phức tạp của mạch số học, lặp song song lượng tử và độ khó của bài toán vector gần nhất. Bài toán vector gần nhất cũng liên quan đến mật mã dựa trên lưới. OpenAI cho biết Astra còn tìm ra phản ví dụ trong lý thuyết đồ thị cực trị, qua đó giải thêm 2 bài khác của Erdős.

Trọng tâm của đợt công bố lần này là bộ chứng chỉ Lean. Theo OpenAI, do kernel của Lean chỉ kiểm tra theo cơ chế nhị phân rằng một chứng minh có “biên dịch được” hay không, quá trình xác minh hình thức không phụ thuộc vào việc phải tin vào tuyên bố của chính mô hình.

Dù vậy, việc mỗi mệnh đề hình thức có phản ánh đúng nội dung mà bài toán mở đặt ra hay không, cũng như giá trị học thuật thực sự của các kết quả, vẫn cần được giới toán học thẩm định. Cả 10 kết quả lần này hiện cũng chưa qua phản biện đồng cấp.

OpenAI từng đối mặt với tranh cãi tương tự. Năm 2025, Kevin Weil, khi đó là Phó chủ tịch phụ trách khoa học của công ty, từng tuyên bố GPT-5 giải được 10 bài toán của Erdős. Tuy nhiên, Thomas Bloom, người vận hành cơ sở dữ liệu bài toán Erdős, khi đó chỉ trích tuyên bố này là “một sự bóp méo kịch tính”. Theo đánh giá lúc bấy giờ, mô hình mới chỉ dừng ở việc truy ra các bài báo có sẵn, và Kevin Weil sau đó đã xóa bài đăng.

Lần này, phản ứng có phần khác đi. Demis Hassabis, CEO của Google DeepMind, cho rằng đây là một trường hợp dễ gây lúng túng, nhưng Thomas Bloom gọi kết quả của Astra là “tin lớn”. Ông nói đây là bước tiến so với phản ví dụ về khoảng cách đơn vị Erdős do một mô hình nội bộ khác của OpenAI tạo ra, mà ông từng hỗ trợ kiểm chứng vào tháng 5.

Astra hiện vẫn chưa được phát hành. OpenAI cho biết mô hình này được thiết kế để nhiều tác nhân phối hợp trong thời gian dài nhằm xử lý các tác vụ phức tạp, đồng thời là phần tiếp nối hướng nghiên cứu về suy luận ở giai đoạn kiểm tra do nhà khoa học Noam Brown dẫn dắt.

Trong một bài đăng trên X, Noam Brown gọi kết quả lần này là “một bước tiến quan trọng của suy luận khoa học”. OpenAI cho biết con người đã biên tập đầu ra của mô hình thành bài báo hoàn chỉnh, nhưng phần lập luận toán học cốt lõi là do Astra tạo ra.

Chi phí token cho 10 lời giải được nêu ở mức khoảng 2.000 USD, tính theo biểu phí API của GPT-5.6 Sol. Sam Altman gần đây cũng đã trình diễn Astra với các nhà hoạch định chính sách tại Washington. Dù vậy, OpenAI cho biết vẫn chưa quyết định thời điểm phát hành, mức giá cũng như việc có tích hợp mô hình này vào GPT-6 hay không.

Ngay cả khi được phát hành, Astra vẫn phải trải qua quy trình thẩm định an toàn AI ở cấp liên bang, tương tự thủ tục từng làm chậm kế hoạch ra mắt GPT-5.6. Ở chiều ngược lại, Liên đoàn Toán học Quốc tế ủng hộ Tuyên bố Leiden và cảnh báo rằng các công ty AI đang “sử dụng nghiên cứu công khai mà không có sự đồng ý, né tránh phản biện đồng cấp, đồng thời đe dọa tính toàn vẹn của chứng minh và việc ghi nhận tác giả”.

Fernando Borretti, một kỹ sư phần mềm, nhận định những lập luận phòng vệ lâu nay của giới toán học có thể không còn phát huy hiệu quả, và AI có thể làm thay đổi tuyến đầu của nghiên cứu toán học. Theo các nguồn tin, công bố của OpenAI đang thổi bùng cuộc tranh luận mới về tiêu chuẩn thẩm định và cách tiếp nhận các kết quả toán học do AI tạo ra, cũng như về bản quyền và đạo đức nghiên cứu.