Formalizing zeta and L-functions in Lean

Loeffler, David; Stoll, Michael

doi:10.46298/afm.15328

数学 > 数论

arXiv:2503.00959 (math)

[提交于 2025年3月2日 (v1) ，最后修订 2025年6月25日 (此版本， v4)]

标题：形式化 zeta 和 L-函数在 Lean 中

标题： Formalizing zeta and L-functions in Lean

Authors:David Loeffler, Michael Stoll

摘要：黎曼zeta函数，以及更一般地，狄利克雷字符的L函数，是数论中研究的核心对象之一。我们报告了一个项目，旨在在Lean的“Mathlib”库中形式化这些对象的理论，包括对狄利克雷关于算术级数中的素数定理的证明以及黎曼假设的形式化陈述。

摘要： The Riemann zeta function, and more generally the L-functions of Dirichlet characters, are among the central objects of study in number theory. We report on a project to formalize the theory of these objects in Lean's "Mathlib" library, including a proof of Dirichlet's theorem on primes in arithmetic progressions and a formal statement of the Riemann hypothesis

评论：	最终版本，将发表于《形式化数学年鉴》
主题：	数论 (math.NT) ; 形式语言与自动机理论 (cs.FL); 计算机科学中的逻辑 (cs.LO)
引用方式：	arXiv:2503.00959 [math.NT]
	(或者 arXiv:2503.00959v4 [math.NT] 对于此版本)
	https://doi.org/10.48550/arXiv.2503.00959
期刊参考：	Annals of Formalized Mathematics, Volume 1 (July 15, 2025) afm:15328
相关 DOI:	https://doi.org/10.46298/afm.15328

提交历史

来自： David Loeffler [查看电子邮件]
[v1] 星期日， 2025 年 3 月 2 日 16:53:20 UTC (12 KB)
[v2] 星期三， 2025 年 3 月 5 日 17:05:01 UTC (12 KB)
[v3] 星期四， 2025 年 6 月 12 日 15:16:29 UTC (13 KB)
[v4] 星期三， 2025 年 6 月 25 日 20:10:42 UTC (436 KB)

数学 > 数论

标题：形式化 zeta 和 L-函数在 Lean 中

标题： Formalizing zeta and L-functions in Lean

提交历史

获取论文：

参考文献与引用

收藏

文献和引用工具

与本文相关的代码，数据和媒体

演示

推荐器和搜索工具

arXivLabs：与社区合作伙伴的实验项目

数学 > 数论

标题： 形式化 zeta 和 L-函数在 Lean 中 显示英文标题

标题： Formalizing zeta and L-functions in Lean

提交历史

获取论文：

参考文献与引用

BibTeX 格式的引用

收藏

文献和引用工具

与本文相关的代码，数据和媒体

演示

推荐器和搜索工具

arXivLabs：与社区合作伙伴的实验项目

标题：形式化 zeta 和 L-函数在 Lean 中