Bendi新闻
>
陶哲轩上新项目:Lean中证明素数定理,研究蓝图都建好了

陶哲轩上新项目:Lean中证明素数定理,研究蓝图都建好了

9月前

机器之心报道

编辑:陈萍

借助 Lean,陶哲轩又开始了新的项目。


「由 Alex Kontorovich 和我领导的一个新的 Lean 形式化项目刚刚正式宣布,该项目旨在形式化素数定理(prime number theorem,PNT)的证明,以及伴随而来的复分析和解析数论的支持机制,并计划给出进一步的结果如 Chebotarev 密度定理。」著名数学家陶哲轩在个人博客中写道。


素数定理是数学中的一个重要定理,描述了素数在自然数中的分布规律,该定理在数论中是一个比较重要的研究方向。

形式化证明本质上是一种计算机程序,但与 C++ 或 Python 中的传统程序不同,证明的正确性可以用证明助手(比如 Lean 语言)来验证。举例来说,陶哲轩在论文《A MACLAURIN TYPE INEOUALITY》中给出的证明只有不到一页,但形式化证明使用了 200 行 Lean 语言。


而陶哲轩的合作者 Alex Kontorovich 也是一位非常著名的数学家,现为罗格斯大学数学系特聘教授,主要研究方向是数论。


目前,这两位数学家合作的 Lean 形式化项目「PrimeNumberTheoremAnd」已经上传到 GitHub 上。


项目地址:https://github.com/AlexKontorovich/PrimeNumberTheoremAnd

因为该项目刚建立不久,陶哲轩以及 Alex Kontorovich 还为此构建了一幅蓝图:


蓝图地址:https://alexkontorovich.github.io/PrimeNumberTheoremAnd/web/

可以看出该蓝图包含 5 个部分:

第一部分介绍了项目的首要目标是在 Lean 中证明素数定理。他们表示该问题仍然是 Wiedijk 列出的需要形式化的 100 个定理中突出的问题之一。值得注意的是,PNT 之前已被形式化过,由 Avigad 等人在 Isabelle 中完成。而该项目的目标是将这项工作扩展到级数中的素数(Dirichlet 定理)、Chebotarev 密度定理等等。

目前,完成上述目标可以考虑下面三种方法:

最快的是 Michael Stoll 提出的「欧拉积」项目,该项目对 PNT 的证明只缺少 Wiener-Ikehara Tauberian 定理(对应第二部分)。

第二种是开发一些复分析,包括在矩形上的残差计算(residue calculus on rectangles)、参数原理(argument principle)和 Mellin 变换,从而得出一个仅包含渐近公式的素数定理(PNT)的证明(对应第三部分)。

第三种方法,也是三种方法中最通用的一种,包括阿达马因子分解定理、Hoffstein-Lockhart 等过程(对应第四部分)。

最后一部分是基本推论。

其实回顾陶哲轩以往的研究,他都多次都提到过 Lean。简单来讲,Lean 是一种可帮助数学家验证定理的编程语言,用户可以在其中编写和验证证明。相比初代 Lean,现在最新的 Lean 4 版本进行了多项优化,包括更快的编译器、改进的错误处理和更好的与外部工具集成的能力等。现在,陶哲轩他们又将该工具用于素数定理的形式化证明,可见 Lean 已成为数学研究中的得力助手。





© THE END 

转载请联系本公众号获得授权

投稿或寻求报道:[email protected]


微信扫码关注该文公众号作者

来源:机器之心

相关新闻

跨越300多年的接力:受陶哲轩启发,数学家决定用AI形式化费马大定理的证明陶哲轩看了都直呼内行!谷歌等用LLM自动证明定理拿顶会杰出论文,上下文越全证得越好陶哲轩最新采访:AI将颠覆数学界!用Lean规模化,成百上千条定理一次秒杀黎曼猜想显著突破!陶哲轩强推MIT、牛津新论文,37岁菲尔兹奖得主参与;恋爱时,学会关爱自己可以让两个人都更加幸福|本周值得读陶哲轩:不懂数学别想靠ChatGPT飞升!解析数论大牛获邵逸夫奖,陶哲轩:他的课好难黎曼猜想突破作者首次公开讲解,陶哲轩送上总结传奇大爷拿下“数学界诺贝尔奖”;陶哲轩祝贺:他本应更知名AI将是数学家的得力助手,陶哲轩谈AI在证明过程中的潜力黎曼猜想显著突破!陶哲轩强推MIT、牛津新论文,37岁菲尔兹奖得主参与陶哲轩牛津对谈罗博深:解密DeepMind如何让AI拿到IMO银牌加州理工华人用AI颠覆数学证明!提速5倍震惊陶哲轩,80%数学步骤全自动化建房就给$3万!加拿大小镇喊话:支票都备好了,就等移民搬过来!一位中年妈妈的叛逆:抛夫弃女后,全家居然都变好了陶哲轩赵宇飞学生联手攻下组合数学难题,23年来首次突破秘密打造「AI陶哲轩」 震惊数学圈!谷歌IMO梦之队首曝光,菲尔兹奖得主深度点评一枚「弃子」打破80年黎曼猜想纪录!菲尔兹奖得主MIT大拿联手,陶哲轩转赞4人团队斩获首届AI奥数竞赛百万大奖!AI破解29题陶哲轩惊呆,CMU华人博士荣登第二陶哲轩转赞!40多年「忙碌海狸」数学难题获突破,4万行Coq代码立大功美国酝酿AI领域"登月计划",陶哲轩领衔62页报告重磅发布!陶哲轩等领衔,美国发布《通过人工智能应对全球挑战》报告,聚焦AI在科研中的应用美国酝酿AI「登月计划」,陶哲轩领衔62页报告重磅发布美国酝酿AI「登月计划」,陶哲轩领衔62页报告重磅发布!这本书是对菲尔兹奖得主陶哲轩数学天赋的高度展现!!豆瓣高达9.8分!
logo
联系我们隐私协议©2024 bendi.news
Bendi新闻
Bendi.news刊载任何文章,不代表同意其说法或描述,仅为提供更多信息,也不构成任何建议。文章信息的合法性及真实性由其作者负责,与Bendi.news及其运营公司无关。欢迎投稿,如发现稿件侵权,或作者不愿在本网发表文章,请版权拥有者通知本网处理。