Hacker News 中文摘要

谷歌TPU是专为AI推理设计的芯片，性能优于GPU，是谷歌云未来十年的核心竞争优势。文章探讨了TPU的发展历程、与GPU的区别、性能对比、普及面临的挑战，以及谷歌TPU的生产规模和Gemini 3对芯片行业的影响。

高通宣布Snapdragon 8 Elite Gen 5移动平台将实现同日Linux上游支持，开发者可第一时间获取最新内核支持。这标志着高通在开源生态支持方面取得重要进展，有助于提升开发效率。

Hacker News用户prodigycorp发帖祝大家感恩节快乐，并提到自己已在该社区活跃15年，尽管每年都有人抱怨社区质量下降，但仍感激这个平台。

这本书介绍了函数式语言中的数据结构和算法，重点是通过证明辅助工具Isabelle进行机器验证，涵盖功能正确性和运行时间分析，采用统一的归纳证明方法，所有证明均可在线查看对应理论。

文章指出，在大型语言模型（LLM）盛行的时代，人们正在失去独特的个人表达。作者强调个人声音的珍贵性——它源于生活经历，随时间成熟，能建立信任和认同。过度依赖LLM写作会削弱这种独特价值，即使模仿"你的声音"也无法替代真实表达随人生状态的自然演变。

文章讨论了GPL许可证是否适用于基于GPL代码训练的AI模型的争议。2021年GitHub Copilot推出时，关于GPL条款应传播至AI模型的观点盛行，但到2025年，这种理论已不如当年常见。尽管仍有自由软件支持者坚持这一观点，但AI编程带来的便利已主导了行业趋势。

AI领域两位领军人物Ilya Sutskever和Yann LeCun指出，当前大语言模型已接近极限，行业正从"规模扩张时代"转向"研究创新时代"。Sutskever认为需要回归基础研究，LeCun则主张转向"世界模型"等全新架构。这标志着AI发展路径的重大转变。

Mixpanel针对近期发生的短信安全事件做出回应，表示正在处理该事件，并强调公司始终将保护客户数据安全放在首位，已采取相应措施加强安全防护。

阿瑟·柯南·道尔通过福尔摩斯系列探讨男性心理健康问题,这源于他父亲酗酒导致精神崩溃的个人经历。作为进步作家,他勇敢触及当时被视为禁忌的男性脆弱性话题,在侦探小说中融入了对心理健康的深刻思考。

这篇文章介绍了在Coq中形式化x86架构子集的工作，利用依赖类型、类型类和符号简化了x86语义模型。作者通过具体函数表示位、字节和内存，并将其映射到数学对象以进行定理证明。该模型支持传统汇编语法，并利用Coq定义实现强大的"宏"功能，包括条件、循环、局部变量和带参数的过程。汇编代码可在Coq中生成十六进制字节序列，并具备正确性定理，将机器码与适用于程序验证的分离逻辑公式相关联。