AIGC动态欢迎阅读
放弃5年职业生涯，将100页证明变代码
关键字：定理,数学,解读,数学家,项目文章来源：新智元
内容字数：7550字内容摘要：
新智元报道编辑：Aeneas 好困
【新智元导读】困扰全世界几个世纪的「臭名昭著」谜题——费马大定理，或将被AI攻克？一位英国数学家宣布，即将启动用Lean重现费马大定理证明过程的项目，将100页证明变成代码。从此，世界顶尖数学难题的证明将成为「众包」项目，你我都可以进去添几笔。费马大定理，即将被AI攻克？
而且整件事最意味深长的地方在于，AI即将解决的费马大定理，正是为了证明AI无用。
曾经，数学属于纯粹的人类智力王国；如今，这片疆土正被先进的算法所破译，所践踏。
费马大定理，是一个「臭名昭著」的谜题，在几个世纪以来，一直困扰着数学家们。
它在1993年被证明，而现在，数学家们有一个伟大计划：用计算机把证明过程重现。
他们希望在这个版本的证明中，如果有任何逻辑上的错误，都可由计算机检查出来。
项目地址：https://github.com/riccardobrasca/flt3
3月底，数学家Pietro Monticone激动地表示，自己和同事几乎在leanprover中完成了指数3的费马大定理的形式化。
他们会尽快把形式化过程移植到Mathlib中，以便在FLT项目中使用。
证原文链接：AI攻克费马大定理？数学家放弃5年职业生涯，将100页证明变代码
联系作者
文章来源：新智元
作者微信：AI_era
作者简介：智能+中国主平台，致力于推动中国从互联网+迈向智能+新纪元。重点关注人工智能、机器人等前沿领域发展，关注人机融合、人工智能和机器人革命对人类社会与文明进化的影响，领航中国新智能时代。
