Tóm tắt
OpenAI nói một bản nội bộ của Astra đã tạo ra kết quả mới cho 10 bài toán lâu năm trong toán học và theoretical computer science. Danh sách trải từ high-dimensional sphere packing, binary và spherical codes, non-sofic groups, Connes’s rigidity conjecture, arithmetic circuit complexity, quantum parallel repetition, closest vector problem, Ehrhart’s volume conjecture, Ramsey numbers đến extremal graph theory.
Điểm khác các thông cáo benchmark thường ngày là OpenAI công bố tên bài toán, bản thảo và Lean certificates cho từng kết quả. Con người vẫn tham gia chuẩn bị manuscript và kiểm tra trách nhiệm công bố, nhưng claim trung tâm là phần lập luận toán học do model tạo ra.
Phát hiện chính
- Model tạo lời giải cho các bài toán mà OpenAI mô tả là không có tiến triển chính trong ít nhất một thập kỷ.
- Tổng token cần cho các lời giải thành công được nói là khoảng 2.000 USD theo Sol API rates. Con số này không đồng nghĩa với toàn bộ chi phí nghiên cứu, vì không bao gồm lương, hạ tầng, harness, bài toán thất bại, hay số attempt.
- Mỗi lời giải được chuẩn bị thành manuscript và formalize bằng Lean certificate, giúp cộng đồng có artifact cụ thể để kiểm tra thay vì chỉ đọc claim.
- OpenAI nhấn mạnh vấn đề attribution: nếu proof do AI sinh ra thì gắn toàn bộ công lao cho con người sẽ làm sai lệch bản chất đóng góp.
Ý nghĩa với Dev
Dev không nên đọc tin này như lời hứa rằng model sắp tự giải mọi bài toán production. Bài học thực dụng hơn là pattern hệ thống: model sinh nhiều hướng giải, pipeline kiểm tra và formalize, con người chọn, sửa, công bố và chịu trách nhiệm.
Với những team đang dùng AI cho coding hoặc research nội bộ, câu hỏi nên chuyển từ “model có trả lời được không?” sang “artifact nào chứng minh câu trả lời đó?”. Lean certificate trong toán học tương tự test, typecheck, reproducible benchmark hoặc audit log trong phần mềm: không loại bỏ lỗi, nhưng buộc claim phải để lại dấu vết kiểm tra được.
Phần còn thiếu là transparency quanh quá trình thử. Nếu một hệ thống chỉ công bố 10 case thắng mà không nói đã thử bao nhiêu case, chi phí thật và tiêu chí dừng là gì, người đọc vẫn phải giữ mức tin vừa phải.
Cách đọc tiếp
Hãy mở các manuscript và Lean certificates nếu bạn quan tâm tới phần toán học. Nếu bạn quan tâm tới AI engineering, hãy tập trung vào câu hỏi quy trình: chọn bài toán thế nào, model được phép dùng tool gì, verifier nằm ở đâu, và failure được ghi lại ra sao.