GPT-6 Astra 完成素数间隔不超过 186 的 Lean 形式化证明

OpenAI 发布仓库 PrimeGaps186（https://github.com/openai/PrimeGaps186），其中 GPT-6-Astra 的 Lean 形式化证明了存在无穷多对间隔不超过 186 的相邻素数。Noam Brown 表示在 GPT-6 Astra 的所有用途中最期待科学发现，称 OpenAI 尚未在数学和科学上把该模型推向极限。仓库说明指出 Lean 结果仍依赖三个明确输入公理，被引用的数学估计和数值计算尚未转化为这些输入的 Lean 证明。