OpenAI 8 月 1 日公布 10 项数学与理论计算机科学结果，涉及高维球堆积、编码理论、非 sofic 群、算术电路复杂度、量子复杂性、格密码和极值组合等方向。官方称这些结果由内部版本 Astra 在模型评估期间生成，随后由人类使用同一模型整理为论文，并由模型为每项论证生成 Lean 形式化证书。
这次发布把可读论文、推理说明和可机器检查的形式化证书放在同一证据链中，便于研究者逐步复核，但 OpenAI 同时明确希望数学共同体继续审查、放入学术背景并推进后续研究。形式化证明可以检查特定逻辑系统中的推导是否成立，却不能自动保证问题陈述、建模假设、引用背景和学术意义都没有遗漏。
因此，这批材料适合作为“AI 参与研究并提供可复核产物”的案例，不应直接写成 10 个问题已经完成独立同行评议。研究者使用时仍需检查论文版本、Lean 环境、定义对应关系与外部专家反馈，并把厂商关于生成过程和成本的说明视为官方披露，而不是第三方复现实验。