2026 09 06 HackerNews
SuperTechFans · 科技资讯
2026-09-06 Hacker News Top Stories # Anthropic 团队用 Claude AI 在11天内完成了费马大定理的完整计算机验证，生成了1300万行Lean代码，展示了AI自动形式化复杂数学证明的可行性。 Google Chrome V8引擎存在高危类型混淆漏洞，已被CISA列入已知利用漏洞目录，要求用户限期修复。 Nitter作为Twitter隐私前端替代品，在下架后反而拥有更多可用实例，并提供了运行指南。 美国89%的人认为政府腐败普遍存在，创历史新高，民主党人和独立人士的腐败感知大幅上升。 Mullvad VPN关闭其公共加密DNS服务，转而赞助Quad9基金会，认为支持专业机构更有效。 Statichost.eu提供完全欧洲化的静态网站托管服务，不依赖美国云平台，支持Git部署和隐私合规。 OpenTrailPaper是开源电子墨水自行车电脑固件，支持骑行数据、离线地图和蓝牙传感器，适合阳光下使用。 AI设计电路板的能力通过EEBench V1基准测试评估，Claude Opus 5以61.6%领先，但复杂布线仍需人工。 AI自动处理事故导致工程师失去对系统的实践和直觉，建议引入事故模拟器进行定期演练。 荷兰央行从美国和加拿大运回86吨黄金储备，反映对特朗普政府信任度崩溃，旨在增强危机准备。 1. 形式化费马大定理 (Formalizing Fermat’s Last Theorem) # https://www.anthropic.com/research/formalizing-fermats-last-theorem 在这篇文章中，Anthropic 公司分享了费马大定理（Fermat’s Last Theorem，FLT）的第一个完整计算机验证证明。研究人员 Tianyi Peng 带领的团队利用 Lean 编程语言，利用 Claude AI 系统在短短 11 天内自主完成了这一任务，生成了 1300 万行 Lean 代码，并证明了 29,500 个中间定理。 费马大定理是由数学家皮埃尔・德・费马于 1637 年首次提出的著名猜想，声称对于任何大于 2 的整数 n，不存在正整数 a、b、c 使得 a^n + b^n = c^n。尽管许多数学家尝试证明这一猜想，但直到 1995 年，安德鲁・怀尔斯才提出了第一份正确的证明，且该证明长达 129 页。 在 2004 年，荷兰计算机科学家扬・贝尔赫斯塔提议将怀尔斯的证明进行 “形式化”，即将数学推理转化为计算机可以自动检查的形式。随后，数学家们花费多年时间开发相关方法，最终在 2024 年，帝国理工学院的凯文・巴扎德启动了一个社区项目，旨在使用 Lean 证明助手完成这一形式化过程。 在正式化费马大定理的过程中，Claude AI 在工作中经历了一些初步尝试的失败，然而通过使用 Prove2Me 这一开放的数学形式化协作平台，Claude 的表现显著提高。该平台通过维护定理陈述的有向无环图（DAG），帮助多个代理协同工作，最终在不到两周的时间内完成了证明。 Claude 的证明采用了怀尔斯证明的简化版本，并只依赖于数学的三个标准公理。经过审核，巴扎德对这一自动形式化的成就表示赞赏，认为这一成果标志着自动形式化现代数学文献的重要进展。 这一工作展示了通过 AI 自动形式化复杂数学证明的可行性，未来可能会在较大程度上减轻人类评审新成果的负担。此外，随着 AI 生成的数学证明越来越多，AI 辅助形式化将有助于人类对结果的信心，成为数学界的重要工具。 文章最后提到，费马大定理的形式化证明不仅是对传统数学工作的补充，也为进一步的数学研究和错误纠正提供了新的可能性。Anthropic 和其他实验室也在扩大对外部研究人员的支持，鼓励更多的数学形式化项目。整体而言，AI 在数学形式化领域的应用被认为是一个积极的发展方向，有助于维护数学知识体系的信任。 HN 热度 740 points | 评论 479 comments | 作者：jlebar | 1 day ago # https://news.ycombinator.com/item?id=49568506 建议阅读 Kevin Buzzard 的博客文章，了解这一成就的背景和意义 Kevin Buzzard 承诺为 Lean 数学库做贡献并创建动态文档，而 Anthropic 可能不会做这些 调侃 Kevin 应多带女友旅行，以促进数学进步 建议众筹送 Kevin 去亚马逊部落两个月，可能能证明黎曼猜想和孪生素数猜想 对比项目经费：Kevin 的 5 年 100 万英镑 vs Anthropic 的 11 天，猜测 Anthropic 可能花费更多 输出 6 亿个 token 按 API 价格