π 的无理性指数上界压到 6.0446,证明已用 Lean 4 完整形式化
Michael_D_Moor · x · 2026-10-07
数学家 Michael 当事人在 GitHub 发布 46 页论文(v4,2026 年 10 月 6 日),证明 π 的无理性指数 μ(π) 至多为 6.0446——这是关于 π 被有理数逼近程度的新上界结果。
关键点:
- 仓库同时提供 Lean 4 / Mathlib 形式化(Lake 项目 MuPi,20 个文件、6238 行代码);
- Lean 证明已完整,唯一前提是素数定理(以 θ(x) x 的形式作为显式假设引入);
- 论文尚未经同行评审,v3(10 月 3 日首个公开版)仍可获取,版本间改动已在仓库注明。
这一「论文 + 机器可验证证明」同步发布的形式,是 AI 时代形式化数学工作流的又一实例。
「研究」频道最新
- 发现无法被监督训练:异常检测如何成为自主实验室的筛选器 — bravo_abad · 2026-10-07
- OpenAI 在 GitHub 发布 372 个 AI 生成数学证明,数学界担忧 — The Decoder · 2026-10-07
- Sergio Paniego 公开马德里 Kernel Panic 演讲：多 Harness RL 终极指南 — SergioPaniego · 2026-10-07
- AI 数学再遭质疑：光证定理不够，提出新猜想才是关键 — AvivTamar1 · 2026-10-07
- 3-sum 降到 n^1.999 让人担心数学「丑陋」?换个视角又美了 — thomasahle · 2026-10-07
- NVIDIA 发布 UNREAL:一个模型统一语料检索与 128K 长上下文 — nvidia · 2026-10-07