Tóm tắt
OpenAI công bố một tuyển tập 10 kết quả giải quyết hoặc tạo tiến bộ đáng kể trên các bài toán mở lâu năm trong toán học và theoretical computer science. Công ty nói các kết quả được tạo bởi một bản nội bộ của Astra, model lớn tiếp theo của họ. Sau đó con người hỗ trợ chuẩn bị manuscript bằng cùng model, và các lập luận được formalize bằng Lean certificates trong repo openai/ten-proofs.
OpenAI ước tính tổng số token cần để tìm lời giải cho các bài toán này có chi phí khoảng 2,000 USD theo Sol API rates. Họ cũng công bố narration về quá trình suy luận của model cho từng lời giải.
Các kết quả chính
Danh sách gồm sphere packing trong không gian cao chiều, binary và spherical codes, non-sofic groups, Connes’s rigidity conjecture, lower bound trong arithmetic circuit complexity, quantum parallel repetition, closest vector problem liên quan lattice cryptography, Ehrhart’s volume conjecture, multicolor Ramsey numbers và extremal number conjectures trong graph theory. Một số kết quả gắn với các vấn đề Erdős lâu năm.
OpenAI nhấn mạnh trách nhiệm attribution: nếu một proof do AI tạo hoàn toàn thì gán tác giả là con người sẽ làm sai lệch cách hiểu về đóng góp. Công ty nói họ chịu trách nhiệm về correctness của manuscript và Lean formalization, còn lập luận toán học do hệ thống tạo ra.
Ý nghĩa với Dev
Bài này chưa phải thứ dev áp dụng ngay vào sản phẩm tuần này, nhưng là tín hiệu mạnh cho research agents. Khi model bắt đầu tạo kết quả chuyên môn sâu, bottleneck chuyển sang harness, lựa chọn bài toán, xác minh, formalization và minh bạch quy trình.
Điểm cần thận trọng là denominator. Muốn đánh giá năng lực thật, cộng đồng cần biết tổng số bài toán đã thử, số attempt, chi phí compute/harness và tiêu chí dừng khi model thất bại. Lean certificates giúp phần correctness, nhưng không tự trả lời toàn bộ câu hỏi về quy trình khám phá.