用户名:  密码:   
网站首页即时通讯活动公告最新消息科技前沿学人动向两岸三地人在海外历届活动关于我们联系我们申请加入
栏目导航 — 美国华裔教授专家网科技动向学人动向
关键字  范围   
 
AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码
2024/4/9 10:50:18 | 浏览:722 | 评论:0

AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码

困扰全世界几个世纪的「臭名昭著」谜题——费马大定理,或将被AI攻克?一位英国数学家宣布,即将启动用Lean重现费马大定理证明过程的项目,将100页证明变成代码。从此,世界顶尖数学难题的证明将成为「众包」项目,你我都可以进去添几笔。

费马大定理,即将被AI攻克?

而且整件事最意味深长的地方在于,AI即将解决的费马大定理,正是为了证明AI无用。

曾经,数学属于纯粹的人类智力王国;如今,这片疆土正被先进的算法所破译,所践踏。

AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码

费马大定理,是一个「臭名昭著」的谜题,在几个世纪以来,一直困扰着数学家们。

它在1993年被证明,而现在,数学家们有一个伟大计划:用计算机把证明过程重现。

他们希望在这个版本的证明中,如果有任何逻辑上的错误,都可由计算机检查出来。

AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码
项目地址:https://github.com/riccardobrasca/flt3

3月底,数学家Pietro Monticone激动地表示,自己和同事几乎在leanprover中完成了指数3的费马大定理的形式化。

他们会尽快把形式化过程移植到Mathlib中,以便在FLT项目中使用。

AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码

证明过程大致遵循Wiles的证明,但会略有改动。

用Lean把费马大定理变成代码

当四月到来时,数学家兼程序员Kevin Buzzard将发布这个计划:通过计算机代码,完成费马大定理的证明。

项目在4月上线后,公开的蓝图就会出现在网上,届时,Lean社区的任何人,都可以为形式化证明做出自己的贡献。

AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码

把一个开创性的100页数学证明,变成计算机代码,这个过程容易实现吗?

这当然就要归功于被陶哲轩大加赞赏、沉迷使用的证明工具Lean,它可以让用户把散文式的证明转化为用于测试的规则和逻辑。

AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码

但无论如何,这项工程都不简单,预计将历时多年,而Kevin Buzzard页获得了项目的资金支持。

AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码

大家都明白,这个项目,很可能是迄今为止最复杂的计算机化方式证明之一。

AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码

费马大定理
费马大定理,堪称是史上最精彩的一个数学谜题。

而证明费马AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码大定理的过程,直接就是一部数学史。


我们耳熟能详的费马大定理,由17世纪的法国数学家皮埃尔·德·费马提出。遗憾的是,他未能在有生之年找到证明。

于是,这项起源于三百多年前的难题,直接挑战了人类整整3个世纪,多次震惊全世界,耗尽人类众多最杰出大脑的精力,也让千千万万业余者痴迷。

AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码

这个定理声称,不存在三个正整数a、b、c能满足方程(a^n + b^n = c^n),其中n是任何大于2的整数。

这个证明的难点就在于,数学家很难找出一个否定案例:我们怎么能保证一定不存在这样一个无穷大的整数n,能满足这个方程式呢?

AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码

幸好,对于今天的数学家来说,将无穷大的概念转换成逻辑,并不是什么新鲜事了。

在较为简单的证明中,我们可以依靠归纳法——

一旦某个逻辑对某个数字成立(比如8),那么它对于之后的每一个数(比如9、10、11等)都同样成立,直到无限大。

AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码

然而,费马大定理却是数学界百年来的一块绊脚石。

直到1993年,英国数学家Andrew Wiles用一份长达100页的书面证明,解开了这一谜团。

AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码
计算机为什么无法证明费马大定理?
业界认为原因有三:
1. 计算机无法推导出无穷种
2. 计算机无法证明逻辑正确
3. 计算机可能会出现转瞬即逝的失误
幸好有Lean辅助证明
一份100页的数学证明,无论是对于普通的数学系学生,还是数学家,都不是那么好驾驭的。
好在,我们可以不再依赖传统的证明方法,可以求助于Lean这样的工具。
它是一款基于C++开发的编程工具,专为编写和验证归纳法证明而设计。
如今许多所谓的「人工智能」,不过是巧妙地排列模仿人类语言的文字。但Lean这类计算机辅助的证明,更深入地融合了人类的思维方式,和计算机辅助加强的能力。
AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码
Lean编程工具,进入本科课堂


在伦敦帝国理工学院教数学的Kevin Buzzard,花费了数年时间,利用Lean为学院的整个本科数学课程开发了支持工具。
通过这些工具,学生们可以将课堂上讨论的内容分解成逻辑和数学运算的步骤。
这就仿佛是一个数学证明上的罗塞塔石碑。
同为数学教师的Clarissa Littler,就非常赞同Kevin Buzzard的理念。
她在波特兰社区学院教授离散数学。过去两个学期里,她都在离散数学课上用Kevin Buzzard开发的「Lean经典入门游戏」。
AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码

地址:https://adam.math.hhu.de/
她会用「自然数博弈」,帮学生熟悉数学归纳法的思想,通过「集合论博弈」,让他们习惯于对集合进行推理。
AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码
在这个过程中,学生们对「严格遵循逻辑规则编写证明」,和「用通俗语言解释事物真理」之间的理解差距,就会逐渐弥合。
Littler强调,课程的一大重点,就是让数学基础不太牢固的学生,更自如地用数学家的方式思考,同时更好地理解证明、证据和展示真理的方法。
这种从形式逻辑到规则列表,再到用散文表达的转变,是将项目分解成互相协作的代码片段的关键所在。
AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码
而这一点,在编程和纯数学的交叉领域尤为重要,也正是Lean这样的工具能大放异彩的地方。
Buzzard表示,他希望将费马大定理引发的复杂数学思想转化为可编程的形式。
几个世纪以来,为了证明这个在Buzzard看来「毫无实际意义」的定理,人们开创了许多极具价值的新数学分支。
是的,在Buzzard看来,费马大定理毫无意义,在现实世界中没有任何应用,不过因为这个「臭名昭著」的问题,几个实际来人们产生了大量绝妙的新想法。
如今,将Wiles的100页长的证明转化为计算机能够理解的形式语言和规则,有望为新一代数学家开启计算机辅助证明的大门。
AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码
而这种转换工具,也能够为编程人员提供帮助。
Littler表示,在这一领域,雄心勃勃的项目总是值得尝试的,因为我们都能从学到的经验和编写的程序库中获益。
交互式的定理证明虽然还是一个较新的领域,但Lean社区已经做了许多优秀的工作。
Kevin Buzzard:Lean的布道者

1968年出生的Kevin Mark Buzzard,在算术几何和Langlands程序方面有着深厚的专业造诣。
他目前是伦敦帝国学院的纯数学教授,也是AI工具Lean的「布道者」。
在皇家文法学校读书期间,Kevin Buzzard曾参加了国际数学奥林匹克竞赛,并在1986年赢得铜牌,1987年以满分拿下金牌。
AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码
此后,他在剑桥大学的三一学院完成了数学本科学习,并于1990年获得Senior Wrangler头衔,于1991年获得C.A.S.M.学位。
在Richard Taylor的指导下,他的博士论文「The levels of modular representations」于1995年完成,探讨了数学中的一个复杂领域。
AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码
1998年,他开始在伦敦帝国学院担任讲师,2002年晋升为高级讲师,2004年被任命为教授。
他还曾在哈佛大学(2002年10月至12月)和其他几所著名机构进行访问研究。
因其在数论领域的突出贡献,他在2002年获得了怀特黑德奖,2008年获得了Senior Berwick奖。
2017年,Buzzard发起了一个关于Lean定理证明器的项目和博客,致力于推动在数学研究中使用计算机辅助证明工具。
他还指导了音乐家Dan Snaith(艺名Caribou)完成了关于超收敛Siegel模符号研究的数学博士论文,Snaith因此从伦敦帝国学院获得了博士学位。
2023年10月,Kevin Buzzard在社交媒体上称,自己获得了研究经费,开始用Lean去证明费马大定理。
AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码
Buzzard表示,「十年前,这需要花费无限多的时间」。为了完成这个项目,他将把自己的教学任务搁置五年。
搁置自己的任务,值得吗?
在他的同行、英国诺丁汉大学Chris Williams看来,这种项目可能会产生意想不到的好处,和深远的影响。
「我认为他不太可能在未来五年内正式形式化整个证明,否则就太惊人了。但是,现在的数论和算术几何中,许多工具都无处不在,因此我预计,未来任何实质性的进展都将非常有用。」
对数学研究意义重大


这个项目还揭示了一个更深层次的价值。
随着计算工具的不断进步,数学的不同分支之间,甚至不同学科之间的界限,正变得越来越模糊,这就导致一些几乎无法验证的证明出现了。
比如,京都大学的日本数学家Mochizuki Shinichi编写了一份长达500页的证明,因为太过复杂,花费了数年时间才发表出来,部分原因就是,人们不知道该如何处理它。
从此,我们可能会发现,数学的边界变得越来越模糊。
这不是指真实性或逻辑上的模糊,而是指一个证明中可以融合的不同思想的范围。
Lean可以让数学家们的思想转化为代码,这就让同行更易于理解。看着前人记录的先例,未来的数学家们可以在此基础上继续推进自己的研究。
Buzzard表示,用Lean进行数学写作的特点就是,你可以留下精确陈述但未经证明的结果,而其他人就可以在之后解决它们。
Lean本身就促成了这样一种工作流。
AI攻克费马大定理?数学家放弃5年职业生涯,将100页证明变代码
换言之,费马大定理正准备以「众包」的方式来解决——特别是如果编码工作超出了Buzzard剩余的工作年限。
完成一个数学证明需要整个社区的努力。
也许,在将来,我们能拥有一个类似Genius.com的平台,用于分享和解读数学证明。
参考资料:
https://www.popularmechanics.com/science/math/a60280173/machines-are-on-the-verge-of-tackling-fermats-last-theorema-proof-that-once-defied-them/
https://www.newscientist.com/article/2422601-mathematicians-plan-computer-proof-of-fermats-last-theorem/#Echobox=1710896989




相关栏目:『学人动向
成立2年产出280篇论文,一个顶尖数学家兼亿万富翁和他打造的新型“科学帝国”|纪念吉姆·西蒙斯(1938-2024) 2024-05-17 [3]
KAN核心团队震撼力作!MIT华人用AI首次发现物理学全新方程 2024-05-17 [3]
图灵奖得主辛顿:坐学术冷板凳的30年 2024-05-18 [3]
詹姆斯·西蒙斯麻省演讲:数学,常识和运气 2024-05-16 [51]
“外籍院士”为何在中国井喷? 2024-05-15 [101]
四位数学家打破了一项长达 75 年之久的纪录,找到了一种更密集地堆积高维球体的方法。 2024-05-09 [111]
丘成桐:中国现今数学还没有达到美国20世纪40年代水平 2024-05-06 [222]
钱理群:想起了七十六年前的纪念 2024-05-05 [201]
画家、版画家威尔•巴尼特作品选 2024-05-05 [182]
为导师起草书稿,却意外收获博士论文…… 2024-05-02 [251]
相关栏目更多文章
最新图文:
:美国加大审查范围 北大多名美国留学生遭联邦调查局质询 :天安门广场喜迎“十一”花团锦簇的美丽景象 马亮:做院长就能够发更多论文?论文发表是不是一场“权力的游戏”? :印裔人才在美碾压华裔:我们可以从印度教育中学到什么? :北京452万人将从北京迁至雄安(附部分央企名单) :《2019全球肿瘤趋势报告》 :阿尔茨海默病预防与干预核心讯息图解 :引力波天文台或有助搜寻暗物质粒子
更多最新图文
更多《即时通讯》>>
 
打印本文章
 
您的名字:
电子邮件:
留言内容:
注意: 留言内容不要超过4000字,否则会被截断。
未 审 核:  是
  
关于我们联系我们申请加入后台管理设为主页加入收藏
美国华裔教授专家网版权所有,谢绝拷贝。如欲选登或发表,请与美国华裔教授专家网联系。
Copyright © 2024 ScholarsUpdate.com. All Rights Reserved.