OpenAI công bố lời giải Navier-Stokes và chứng minh hình thức hóa bằng Lean

Hệ thống nội bộ của OpenAI vừa đưa ra lời giải cho bài toán thiên niên kỷ Navier-Stokes, đồng thời công bố chứng minh hình thức hóa bằng ngôn ngữ Lean.

Trong thông báo chính thức, OpenAI cho biết khi có một ngoại lực “mượt” tác động, một khối chất lỏng không nén được trong không gian ba chiều, ban đầu ở trạng thái đứng yên, vẫn có thể hình thành điểm kỳ dị trong khoảng thời gian hữu hạn, trong khi năng lượng của toàn bộ hệ vẫn được giữ ở mức hữu hạn suốt quá trình. OpenAI giải thích rằng kết quả này đáp ứng hai mệnh đề C và D trong bộ đề bài chính thức do Viện Toán học Clay (Clay Mathematics Institute) đưa ra. OpenAI đã công bố cùng lúc bài báo khoa học và chứng minh hình thức hóa bằng Lean.

OpenAI cho biết đã sử dụng một mô hình nội bộ mạnh hơn đáng kể so với GPT-6 Astra, với khoảng 10.000 agent chạy song song trong khoảng 88 giờ để tìm ra lời giải. Trong quá trình xử lý bài toán Navier-Stokes, các agent này đã trao đổi khoảng 2,7 triệu tin nhắn và tạo ra khoảng 130 tỷ token đầu ra, trong khi bước hình thức hóa bằng Lean và kiểm chứng kết quả mất thêm 17 giờ. OpenAI cũng nói rõ công ty không có ý định nộp hồ sơ để nhận giải thưởng thiên niên kỷ từ kết quả này.