π 的无理性指数上界压到 6.0446，证明已用 Lean 4 完整形式化

数学家 Michael 在 GitHub 发布 46 页论文，证明 π 的无理性指数 μ(π) 至多为 6.0446，给出关于 π 被有理数逼近程度的新上界。仓库同时提供 Lean 4 / Mathlib 形式化（Lake 项目 MuPi，20 个文件、6238 行代码），Lean 证明已完整，唯一前提是以 θ(x) ~ x 形式显式引入的素数定理。