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

- 来源：Noam Brown (@polynoamial)
- 发布时间：2026-09-04 02:42
- AIHOT 分数：66
- AIHOT 链接：https://aihot.virxact.com/items/cmtlw5jja0pdrrow5m965czk1
- 原文链接：https://x.com/polynoamial/status/2095583211950833768

## AI 摘要

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

## 正文

Of all the use cases for GPT-6 Astra, I'm most excited for scientific discovery. We at @OpenAI have not pushed it to its limits on math and science.

I look forward to waking up every morning and seeing what new scientific breakthrough someone has made with this model!

### 引用推文

> Lisan al Gaib：New OpenAI repo with a Lean formalization by GPT-6-Astra proves that there are infinitely many pairs of consecutive primes whose distance is at most 186 https:/...