OpenAI cho biết một mô hình tiên tiến nội bộ đã tạo ra hàng trăm kết quả toán học, bao gồm các chứng minh được hình thức hóa bằng Lean và những công trình nguyên bản giải quyết các câu hỏi nghiên cứu còn bỏ ngỏ. Điểm mới nằm ở hai khía cạnh: quy mô của các kết quả tiềm năng và việc sử dụng trợ lý chứng minh tương tác để hình thức hóa, tạo ra các hiện vật có thể kiểm tra thay vì chỉ là lập luận bằng ngôn ngữ tự nhiên. Sự kết hợp giữa suy luận tạo sinh và đầu ra có thể được máy kiểm tra này tạo nên khác biệt, bởi nó mở ra con đường từ ý tưởng ban đầu của mô hình đến một kết quả có thể được xác thực bằng máy, giúp tái lập độc lập nhanh hơn so với những tuyên bố chỉ được trình bày bằng văn bản.

Trong quá khứ, các mô hình tiên tiến thường được đánh giá dựa trên năng lực lập trình và xử lý ngôn ngữ; tạo ra nội dung toán học nguyên bản là bước tiến sang địa hạt sáng tạo và khoa học. Khám phá toán học đòi hỏi đề xuất phỏng đoán mới, xây dựng lập luận không tầm thường và tổng hợp các kết quả hiện có theo cách thúc đẩy tri thức. Khi mô hình tìm ra bổ đề mới hoặc lấp đầy khoảng trống trong những chứng minh phức tạp, chúng đảm nhận vai trò gần với trợ lý nghiên cứu hơn là công cụ dành cho nhà phát triển. Sự chuyển dịch này thay đổi nhóm đối tượng hưởng lợi và cách tích hợp đầu ra của mô hình: từ lập trình viên tăng tốc triển khai sang nhà nghiên cứu đẩy nhanh việc hình thành giả thuyết và xây dựng chứng minh.

Hình thức hóa bằng Lean giúp giảm sự mơ hồ nhưng không loại bỏ nhu cầu xác minh. Chuyển một gợi ý phi hình thức của mô hình thành chứng minh Lean được đặc tả đầy đủ thường đòi hỏi kỹ thuật từ con người: phải lựa chọn định nghĩa, mã hóa bổ đề và điều chỉnh tập lệnh chứng minh. Ngoài ra, hình thức hóa bằng Lean cho thấy các chuỗi phụ thuộc và giả định ẩn nhưng cũng có thể đưa vào những sai sót riêng. Vì vậy, một quy trình vững chắc cần kết hợp kiểm tra chứng minh tự động, kho lưu trữ có thể tái lập với phiên bản môi trường và chuỗi công cụ chính xác, cùng việc chuyên gia độc lập tái lập để xác nhận tuyên bố của mô hình không chỉ đúng trong hiện vật ban đầu.

Các kết quả toán học do AI tạo ra buộc các tổ chức phải xem xét lại quy ước về quyền tác giả và ghi nhận công lao. Nếu một định lý được phát hiện với sự hỗ trợ đáng kể của mô hình, danh sách tác giả nên ghi tên nghiên cứu viên chính là con người, nhà phát triển mô hình, cả hai hay không bên nào? Hồ sơ nguồn gốc cũng quan trọng không kém: cần lưu lại các tập lệnh chứng minh có quản lý phiên bản, điểm kiểm tra mô hình, lời nhắc khởi tạo và chỉnh sửa của con người để người phản biện có thể lần theo quá trình phát triển của ý tưởng. Tạp chí và hội nghị cần cập nhật chính sách nộp bài, yêu cầu công khai rõ việc sử dụng mô hình và xác định cách ghi nhận hoặc từ chối các tuyên bố có nguồn gốc từ AI khi hồ sơ nguồn gốc không đầy đủ.

Các nhóm nên áp dụng những thực hành cụ thể: (1) xem đầu ra của mô hình là bản nháp cần được hình thức hóa và kiểm tra độc lập; (2) quản lý phiên bản tập lệnh chứng minh và lưu lại chính xác mô hình cùng lời nhắc đã sử dụng; (3) xây dựng quy trình đánh giá liên ngành, kết nối chuyên gia lĩnh vực với kỹ sư xác minh; và (4) đầu tư vào công cụ tự động ghi nhận môi trường và chạy lại chứng minh. Nhà tài trợ nên ưu tiên các dự án thu hẹp khoảng cách xác minh và hỗ trợ hạ tầng cộng đồng giúp toán học có máy hỗ trợ có thể tái lập, thay vì chỉ tập trung vào quy mô mô hình hoặc các bộ chuẩn đánh giá.