1637 年，费马在浏览丢番图《算术》拉丁文译本时，曾在第 11 卷第 8 命题旁写道：「将一个破方数分红两个破方数之跟，或一个四次幂分红两个四次幂之跟，或许个别地将一个高于二次的幂分红两个同次幂之跟，这是弗成能的。对于此，我确信我发明一种美好的证法，惋惜这里的空缺处太小，写不下。」这就是有名的费马年夜定理（FLT，也叫费马最后定理）：当整数 n > 2 时，对于 x, y, z 的不定方程 xⁿ + yⁿ = zⁿ 无正整数解。尔后，有数数学家跟数学喜好者都实验过证实这个定理；乃至对该定理的证实一度成为「官方数学家」最爱挑衅的困难之一，这个景象让数学汗青学家霍华德・伊夫斯（Howard Eves）不由得感叹：「费马年夜定理的奇特之处在于它是迄今为止宣布过错证实最多的数学识题。」对费马年夜定理的首个完全证实直到 358 年之后的 1995 年才真正宣布。为此，英国数学家安德鲁・怀尔斯（Andrew Wiles）应用了一系列庞杂的数学东西跟实践。团体而言，怀尔斯的证实树立在模情势跟椭圆曲线之间的深入接洽（即谷山 - 志村料想的一局部）之上，全部证实十分庞杂，论文《Modular elliptic curves and Fermat’s Last Theorem》就有 109 页。克日，伦敦帝国粹院数学教学 Kevin Buzzard 在本人的博客上分享了一个十分风趣的名目：教盘算机懂得费马年夜定理的证实。这项任务能够辅助验证对费马年夜定理的证实，修改此中可能存在疏漏的局部。固然盘算机还不完整懂得，但也确切获得了一些停顿。这篇博客在 Hacker News 上吸引了大批探讨，良多人都分享了本人的看法或阅历，尤其是对于数学情势化的主要性。以上截图均来自 Hacker News 跟谷歌翻译，更多探讨请拜访：https://news.ycombinator.com/item?id=42399397以下是 Buzzard 教学的博客全文（原文段落较长，这里停止了恰当拆分跟调剂）。费马年夜定理 —— 停顿怎样？我曾经花了两个月时光来教盘算机懂得马年夜定理（FLT）的一个证实。年夜局部的「停顿怎样」说明起来都相称繁琐且技巧性：长话短说，怀尔斯证实了「R=T」定理，而到现在为止的年夜局部任务都是教盘算机懂得什么是 R 跟 T；咱们依然还不实现这两者中任何一个的界说。然而，我的博士生 Andrew Yang 曾经证实了咱们须要的形象可交流代数成果（「假如形象环（abstract rings）R 跟 T 满意很多技巧前提，则它们相称」），这是令人高兴的第一步。咱们应用的体系是 Lean 及其数学软件库 mathlib，该软件库由 Lean 证实器社区保护。假如你对 Lean 跟数论有所懂得，能够斟酌浏览奉献指南、检查名目仪表板并认领一个成绩。上面是一些相干链接：蓝图跟停顿：https://imperialcollegelondon.github.io/FLT/blueprint/Lean：https://lean-fro.org/mathlib：https://github.com/leanprover-community/mathlib4奉献指南：https://github.com/ImperialCollegeLondon/FLT/blob/main/CONTRIBUTING.md名目仪表盘：https://github.com/orgs/ImperialCollegeLondon/projects/102成绩：https://github.com/ImperialCollegeLondon/FLT/issues如前所述，咱们曾经停止了两个月。然而，咱们曾经有一个我以为值得分享的风趣故事了。谁晓得这能否预示着某个将来。咱们的目标并不是情势化 1990 年月谁人 FLT 证实。自那当前，曾经有良多人（Diamond/Fujiwara、Kisin、Taylor、Scholze 等人）对该证实停止了泛化跟简化。我的局部念头是要证实这些更通用、更无力的成果。为什么这是由于假如 AI 真的能够变更数学（有可能），而且 Lean 被证实是一个主要的构成局部（也有可能），那么盘算机将可能更好地辅助人类冲破古代数论的界线。对这种情势化任务，盘算性能够以它们懂得的方法来取得要害的古代界说。怀尔斯的原始证实中不应用的一个观点，在咱们正在情势化的证实中应用了，它就是晶体上同调（crystalline cohomology）。这是 20 世纪六七十年月在法国巴黎开展起来的实践，其基本是由数学家 Berthelot 依据另一位数学家 Grothendieck 的思维搭建的。基础思维是经典指数跟对数函数在微分多少何（比方 Lie 代数跟 Lie 群）施展要害感化，特殊是在懂得德拉姆上同调（de Rham cohomology,）中，不外它们在更多的算术情形下不起感化（比方在特点 p 中）。20 世纪六十年月，Roby 在一系列出色的论文中提出了「除幂构造」（divided power structures），在构建可用于算术情形的类函数中施展了至关主要的感化。注：咱们要想教盘算机晶体上同调，起首须要教它除幂实践。数学范畴的研讨者 Antoine Chambert-Loir（简称 Antoine）跟 Maria Ines de Frutos Fernandez（简称 Maria Ines）始终在教 Lean 除幂实践，而全部炎天，Lean 都时而呈现一种令人末路火的情形：它会埋怨尺度文献中工资提出的论证，并经由细心检讨发明工资论证有待改良，特殊是 Roby 的任务中有一个要害引理仿佛不准确。当 Antoine 告知我这件事时，他感到我会以为这很风趣，而他收到的复兴中一长串年夜笑的心情标记确切证明了这一点。但是，Antoine 比我更专业，以为我不该该发推探讨这个成绩（横竖我也不发，我曾经摈弃了推特并转向了交际平台 bluesky），而应当实验处理这个成绩。咱们以完整差别的方法来处置这个成绩，Antoine 把它列入了本人的任务清单，而我却完整疏忽了它，只是偶然向人们说起这个证实有成绩，是弱证实。我之以是说是弱证实，是由于这一察看必需放在某种配景下。依据我现在对数学的察看（作为情势主义者），当 Antoine 发明这个成绩时，全部晶体上同调节论就从文献中消散了，并带来宏大的附带侵害（比方数学家 Scholze 的大批任务就消散了，整本的册本跟论文都子虚乌有）。但这种消散只是临时的，晶体上同调在现实意思上并不过错。这些定理毫无疑难依然是准确的，只是就我而言，证实是不完全的（或许至少 Antoine 跟 Maria Ines 遵守的证实不完全）。因而咱们的任务就是修改它们。我想夸大的是，我跟 Antoine 都很明白，即便旁边引理是过错的，重要成果的证实固然能够修改，这是由于从 20 世纪 70 年月以来晶体上同调就失掉了普遍应用。假如它有成绩，早就该裸露出来了。我交换过的每个专家都批准这一点，有多少位乃至以为我在小题年夜做。但兴许他们不清楚情势化在实际中究竟象征着什么：你不克不及只是说「我信任它能够修改」，你必需真正地修改它。别的，Roby、Grothendieck 跟 Berthelot 都曾经逝世了，咱们无奈从这些本来的专家那边直接追求辅助。对更多技巧细节感兴致的人能够先看这里：Berthelot 的论文并不重新开端开展除幂实践，他应用了 Roby 的「Les algebres a puissances divisees」，1965 年在 Bull Sci Math 上宣布。该论文的引理 8 仿佛是过错的，并且怎样修改证实也没阐明白。该引理的证实过错援用了 Roby 1963 年 Ann Sci ENS 论文中的另一个引理。其准确的表述是「Gamma_A (M) tensor_A R = Gamma_R (M tensor_A R)」，但此中一个张量积在利用中不测离开。这就攻破了 Roby 对于「模（module）的除幂代数存在除幂］的证实，从而禁止咱们界说环 A_{cris}。以是，正如我所言，Antoine 正努力于处理这个成绩，而我只是在向专家们八卦闲谈，并且我犯了一个错：在伊斯灵顿的一家咖啡店告知了時枝正（Tadashi Tokieda）这件事，他回到斯坦福后向 Brian Conrad 提到了这件事，而后 Conrad 就开端在我的收件箱里问我晶体上同调有成绩究竟是怎样回事。我说明了这个成绩的技巧细节，Conrad 批准这似乎确切是一个成绩，而后他开端思考。多少个小时后，他复兴了我，并指出，在 Berthelot-Ogus 的对于晶体上同调的著述的附录中，存在对「模的个别除幂代数存在除幂」这个断言的另一个差别的证实，并且 Conrad 以为这个方式不成绩。证实又返来了！这差未几就是故事的全体。上个月我拜访了伯克利，跟 Arthur Ogus 共进午餐，我 90 年月在那边做博士后的时间就意识他了。我许可过 Arthur，给他讲一个他怎样救命费马年夜定理的故事，用饭的时间我告知他，他的附录怎样把我从窘境中救了出来。他的答复是「哦！谁人附录有多少个过错！但不要紧，我想我晓得怎样修改它们。」在我看来，这个故事标明，人们在编写古代数学文档方面做得很差。仿佛有良多货色是「专家们已知的」，但却并不失掉准确的文档化。这些专家们分歧以为，主要的主意充足强盛，能够禁受住如许的袭击，但现实产生的细节可能并不像人们冀望的那样。对我来说，这只是人类想要准确记载数学的浩繁起因之一，即在情势体系中，过错的可能性要小多少个数目级。但是，年夜少数数学家都不是情势主义者，对这些人，我须要以差别的方法阐明我的任务的公道性。对那些数学家而言，我以为教会呆板懂得咱们的论证是让呆板本人做这件事的要害一步。在此之前，咱们仿佛注定要手动修改工资过错。不外，这个故事确切有一个美满的终局 —— 两周前，Maria Ines 在剑桥数学情势化研究会（Cambridge Formalization of Mathematics seminar）上宣布了一个对于除幂的情势化的报告。依据这个报告，我的懂得是这些成绩当初曾经失掉处理了。以是咱们现实上又回到了正轨。直到下一次文献让咱们扫兴……参考链接：https://xenaproject.wordpress.com/2024/12/11/fermats-last-theorem-how-its-going/https://news.ycombinator.com/item?id=42399397© THE END 转载请接洽本大众号取得受权投稿或追求报道：[email protected] ]article_adlist--> 　　申明：新浪网独家稿件，未经受权制止转载。 -->