作者:王方 来源:中国科学报 发布时间:2024/3/24 15:27:32
选择字号:
数学家计划计算机证明费马大定理

 

费马大定理是一个关于数字的著名定理,几个世纪以来一直困扰着数学界。现在,数学家希望开发一种计算机证明费马大定理的方法。这是一个雄心勃勃、为期数年的项目,旨在展示计算机辅助数学证明的潜力。

  ?

皮埃尔·德·费马    图片来源:GRANGER Historical Picture Archive/Alamy

法国数学家皮埃尔·德·费马在1640年左右首次提出费马大定理,即当整数n>2时,关于x、y、z的方程xn+yn=zn没有正整数解。费马在一本书中潦草地写下这一定理,并加了一句:“我发现了一个真正了不起的证明,可惜这里空白处太小了,容不下。”

直到1993年,当时在美国普林斯顿大学的安德鲁·怀尔斯才宣布自己的证明,轰动了数学界。这份长达100多页的证明包含了如此高级的数学知识,以至于他的数学同仁花了两年多才验证它没有任何错误。

许多数学家希望,通过将证明翻译成计算机可读的语言,以加快检验和最终写出证明的速度。这种形式化的过程可以让计算机立即发现逻辑错误,并有可能将这些定理用作其他证明的构建块。

但是,将现代证明形式化本身就很棘手且耗时,因为它们所依赖的许多现代数学尚未实现机器可读。由于这个原因,将费马大定理形式化一直被认为是遥不可及的。

英国剑桥大学的Lawrence Paulson表示:“仅仅是为了首先证明它,就被视为一个费力劳神的证明。”

现在,英国帝国理工学院的Kevin Buzzard和同事宣布接受挑战。他们试图用一种名为Lean的编程语言将费马大定理形式化。

“费马大定理毫无意义。它在现实世界中没有任何应用,无论是理论上还是实践上。”Buzzard说,“但它是一个非常棘手、‘臭名昭著’的问题。几个世纪以来,人们为了解决这个问题,产生了大量精彩的新想法。”

Buzzard希望,通过将这些想法形式化,包括数论中的常规数学工具,如模形式和伽罗瓦理论,将有助于其他研究人员,他们的工作目前远远超出了计算机辅助的范围。

英国诺丁汉大学的Chris Williams说:“这类项目可能会产生深远而意想不到的好处和结果。”

证明本身将大致遵循怀尔斯的方法,稍加修改。项目即将在4月上线,会在网上提供一个公开可用的蓝图。这样,来自Lean快速增长社区的任何人都可以为形式化证明的一部分做出贡献。“10年前,这可能需要无限的时间。”Buzzard说。

“我认为他不太可能在未来5年内将整个证明形式化。但由于现在许多工具在数论和算术几何中无处不在,我预计未来在这方面的任何实质性进展都将非常有用。”Williams说。

 
版权声明:凡本网注明“来源:中国科学报、科学网、科学新闻杂志”的所有作品,网站转载,请在正文上方注明来源和作者,且不得对内容作实质性改动;微信公众号、头条号等新媒体平台,转载请联系授权。邮箱:shouquan@stimes.cn。
 
 打印  发E-mail给: 
    
 
相关新闻 相关论文

图片新闻
“研0”科研入门需要作哪些准备? 中国科学家首次发现“无摩擦的冰”
冰表面长啥样?原子级分辨图像揭晓答案 北方中纬高频雷达网发布首批科学探测结果
>>更多
 
一周新闻排行
 
编辑部推荐博文