ζ(5) 无理性获证明，数小时内完成 Lean 形式化

数学家 Aabir Fauzan 的预印本很可能证明了 ζ(5) 是无理数，这是 zeta 函数奇数值性质研究的重大进展。Elliot Glazer 与 Alex Kontorovich 等数学家转发认可，Moritz Firsching 随即在数小时内基于 Lean 4 / Mathlib 完成该证明的完整形式化，代码已开源在 GitHub 的 Zeta5 仓库中。

2026-09-24 ~ 2026-09-24 · 4 条相关

• zeta(5) 或已被证明无理数,作者用 Astra 验证论证正确性 — aran_nayebi · 2026-09-24
• ζ(5) 被证明是无理数,Lean 形式化验证数小时内完成 — ctjlewis · 2026-09-24
• 数学家宣称 ζ(5) 无理性证明，Lean 形式化已公开在 GitHub — AlexKontorovich · 2026-09-24

另有 1 条近重复转述:AlexKontorovich