OpenAI 发布 PrimeGaps186：带显式公理边界的素数间隔 Lean 形式化与数值证书

OpenAI 公开了素数间隔上界 186 的 Lean 4 形式化与 Python 数值证书。仓库明确说明 Lean 结果仍依赖 3 个显式输入公理，数值估计也尚未全部转化为 Lean 证明；项目 metadata 记录了 GPT-6 Astra / Codex agent 参与、Comparator、Nanoda 与 Lean kernel 检查。