费马大定理，一个数学史上的经典难题，曾经困扰着无数数学家几个世纪。直到1993年，英国数学家Andrew Wiles终于用长达100页的书面证明解开了这个谜团。但如今，另一位数学家Pietro Monticone宣布，他将启动一个项目，用Lean重现费马大定理的证明过程，将证明变成代码。
这个项目的意义深远，因为费马大定理的证明正是为了证明AI的无用。数学曾经是纯粹的人类智力领域，但如今，先进的算法正在破解这片领域。费马大定理的证明过程大致遵循Wiles的证明，但会有一些改动。数学家兼程序员Kevin Buzzard将在4月发布这个计划，通过计算机代码完成费马大定理的证明。
这个过程并不容易，但Lean这样的工具让这一切成为可能。Lean是一款专为编写和验证归纳法证明而设计的编程工具，可以将散文式的证明转化为逻辑和规则。Kevin Buzzard花费数年时间为伦敦帝国理工学院的本科数学课程开发了支持工具，让学生们可以更好地理解数学证明的过程。
这个项目的意义不仅在于解决费马大定理这一经典难题，更在于揭示了数学界的新趋势。随着计算工具的进步，数学的不同分支之间的界限变得模糊，这可能导致一些无法验证的证明出现。Lean可以让数学家们的思想转化为代码，让同行更易于理解。费马大定理的解决可能以众包的方式进行，需要整个社区的努力。
在未来，或许我们会看到一个类似Genius.com的平台，用于分享和解读数学证明。费马大定理的攻克，将为新一代数学家开启计算机辅助证明的大门，推动数学研究迈向新的高度。费马大定理的证明，不仅是一项数学成就，更是一次对人类智慧和技术的挑战。
