我们正处于一个信息大暴发的时代,每天都能产生数以百万计的新闻资讯!
虽然有大数据推荐,但面对海量数据,通过我们的调研发现,在一个小时的时间里,您通常无法真正有效地获取您感兴趣的资讯!
头条新闻资讯订阅,旨在帮助您收集感兴趣的资讯内容,并且在第一时间通知到您。可以有效节约您获取资讯的时间,避免错过一些关键信息。
本文转自:中国科学报
本报讯 费马大定理是一个关于数字的著名定理,几个世纪以来一直困扰着数学界。现在,数学家希望开发一种计算机方法,用来证明费马大定理。这是一个雄心勃勃、为期数年的项目,旨在展示计算机辅助数学证明的潜力。
法国数学家皮埃尔·德·费马在1640年左右首次提出费马大定理,即当整数n>2时,关于x、y、z的方程xn+yn=zn没有正整数解。费马在一本书中潦草地写下这一定理,以及那句著名的话:“我发现了一个真正了不起的证明,但这里的空白太小了,容不下。”
直到1993年,美国普林斯顿大学的安德鲁·怀尔斯宣布了自己的证明,并轰动了数学界。这份长达100多页的证明包含了如此高级的数学知识,以至于他的同事花了两年多来验证其设有任何错误。
许多数学家希望,通过将证明翻译成计算机可读的语言,可以加快检验和最终编写证明的速度。这种形式化的过程可以让计算机立即发现逻辑错误,并有可能将这些定理用作其他证明的基础。
但是,将现代证明形式化本身就很棘手且耗时,因为它们所依赖的许多现代数学尚未实现机器可读。由于这个原因,将费马大定理形式化一直被认为是遥不可及的。
现在,英国帝国理工学院的Kevin Buzzard和同事宣布接受这一挑战。他们试图用一种名为Lean的编程语言将费马大定理形式化。
“费马大定理毫无意义。它在现实世界中没有任何应用,无论是理论上还是实践上。”Buzzard说,“但它是一个非常棘手、‘臭名昭著’的问题。几个世纪以来,人们为了解决这个问题,产生了大量精彩的新想法。”
Buzzard希望通过将这些想法形式化,包括数论中的常规数学工具,如模形式和伽罗瓦理论,从而帮助其他研究人员。他们的工作目前远远超出了计算机辅助的范围。
英国诺丁汉大学的Chris Williams说:“这类项目可能会获得意想不到的好处并产生深远的影响。”
证明本身将大致遵循怀尔斯的方法并稍加修改。该项目即将在4月上线,同时会在网上提供一个公开可用的蓝图。这样,来自Lean快速增长的社区的任何人都可以为形式化证明作出贡献。“10年前,这可能需要无限的时间。”Buzzard说。
“我认为他不太可能在未来5年内将整个证明形式化。但由于现在许多工具在数论和算术几何中非常普遍,我预计未来在这方面的任何实质性进展都非常有用。”Williams说。
(王方)
以上内容为资讯信息快照,由td.fyun.cc爬虫进行采集并收录,本站未对信息做任何修改,信息内容不代表本站立场。
快照生成时间:2024-03-25 08:45:13
本站信息快照查询为非营利公共服务,如有侵权请联系我们进行删除。
信息原文地址: