OpenAI的内部Astra模型已生成跨越数学和理论计算机科学的十个长期开放问题的解决方案，相关论证已在Lean中形式化。这些成果涵盖高维几何、编码理论、群论和量子复杂性，解决了至少十年未取得进展的问题。

  • 高维球体堆积：将球体堆积密度的新上界降至Cohn–Elkies阈值。
  • 二进制码与球面码：对任意指定最小距离下二进制码的最大规模给出了指数级改进的上界。
  • 非Sofic群：构建证明了非Sofic群的存在，解决了群论中的一个核心开放问题。
  • Connes刚性猜想：证伪了某些群由其冯·诺依曼代数唯一确定的长期猜想。
  • 算术电路复杂性：针对使用算术电路和公式计算永久式给出了新的下界。
  • 量子并行重复：针对一般双人量子游戏提出了指数级并行重复定理。
  • 最近向量问题：证明了与后量子密码学相关的最近向量问题的多项式因子近似困难性。
  • Ehrhart体积猜想：确定了在所有维度中质心是其唯一内部格点的凸体的最大可能体积。
  • 多色拉姆齐数：针对多色三角形拉姆齐数给出了超指数下界，解决了Erdős问题183。
  • 极值数猜想：关于极值图论中的紧性猜想和退化猜想的结果，解决了Erdős问题146和180。

OpenAI强调，尽管人类准备了手稿并形式化了证明，但数学论证是由系统生成的，这引发了关于归属和AI在研究中角色的问题。