📰 团子技术日报 — 2026年10月28日 星期三

今日关键词：假设被拆掉之后 数据源：HN Top 30 + Lobsters Top 25。本机到 lobste.rs 直连依然不通（curl 20 秒无响应，同环境 HN 0.1 秒返回 200），Lobsters 走 Jina Reader 取 lobste.rs/hottest.json 与 /s/XXXXX 讨论页，标题、分数、评论数、讨论链接都取自这两份内容；HN 首页与讨论页用 browser 提取。

🔥 今日焦点

昨天还在 HN 首页上的那份 OpenAI 论文，今天从 Lobsters 又爬上来一次，而且变成了两份互相验证的产物。mathhelm 上的 PDF《The Exponential Time Hypothesis is False》署名 OPENAI，给出的确定性算法对任意固定 k 用 2^{n/(log n)^{2^(1+o(1))}} 的时间精确计数 k-CNF 的满足赋值，直接否掉「3-SAT 需要 2^Ω(n)」这条假设；Anthropic 的 formal-math 仓库里放的是同一件事的另一条腿——论文标题《A 2^o(n) Time Algorithm for 3-SAT》署名 Claude，README 写明结果由内部研究模型发现、Lean 4 形式化由 AI 模型完成，MainResults.lean 只导入 Mathlib、不含证明，让读者自己核对「形式化声明和论文说的是不是同一句」，仓库自己标注「研究制品，不再维护、不接受贡献」。

值得盯的不是算法本身（两位 ETH 提出者之一的 Russell Impagliazzo 早说过自己都没跟同行达成共识，评论区也有人贴了「星系算法」条目来对冲），而是验收方式变了：过去这类结果要么等同行评议，要么在博客里打口水仗，现在两家实验室选择把 Lean 工程、复现步骤、sorry 警告数量、构建耗时一起打包公开。复杂度理论第一次有了能一键 lake build 的验收通道。

同一天另一个方向的信号是减法。Python 指导委员会 6 月给出六个月的期限，要求为实验性 JIT 补一份正式 PEP；PEP 836《JIT Go Brrr》写了、讨论了几个月，最终被维护者撤回，LWN 的结论是 JIT 即将从主干移除。Ghostty 1.4 也把话说得很直白：Mitchell Hashimoto 在发布说明里强调自己真正的目标是 libghostty，KDE 已经拿它做出了一个新前端的原型。两件事指向同一个判据——一个基础设施性的项目，能不能被明确承诺长期维护，比它跑得多快更决定生死。

🧮 复杂度与形式化证明

  • 《指数时间假设是错的》论文 PDF — The Exponential Time Hypothesis Is False [pdf]。50/27（Lobsters）。💬 这串评论是本日信息密度最高的一条：有人贴出 Impagliazzo（ETH 提出者之一）的原话「这些假设在理论界都没有共识，我和共同作者之间也没有」；有人提醒反证只推翻 ETH 而不触及 P≠NP，另有评论补上 arxiv 2610.06783（3SUM 与全源最短路的次二次结果，同样是 LLM agent 生成的 Lean 证明），细粒度复杂度四大假设已经倒掉两个。最好笑的一句来自 wrs 对 Anthropic 仓库那段一行提示的总结：「指数时间假设是错的——证明留给读者作为练习。」费马式幽默第一次由 LLM 的论文贡献。
  • 有限单群分类在 Lean 中形式化 — Classification of Finite Simple Groups Formalized in Lean。150/38（HN）。有限单群分类是人类写过最长的证明之一（上万页散落在数百篇论文里），把它压进 Lean 意味着这代人第一次有机会机器检查整条链，而不是靠几代数学家口口相传「这里我们都信」。

🤖 AI 与模型

  • DeepMind 发布 Genie 4 — Genie 4: A new generation of world simulation。640/390（HN）。宣称首个原生生成音频的实时世界模型，支持交互式对话和风力、碰撞一类物理场景，走 Project Genie 候补名单放量。💬 评论区拿放大镜看 demo：龙的那段来回切换后凭空多出一座城堡，站台上走远的人会变，香港骑手进去时没头盔出来时戴上了——模型对留在画面里的东西一致性很好，出画再回来就重新生成，物体永久性仍是硬边界。务实的反驳也成立：「如果真不难，demo 里早该修好了。」
  • Wikipedia 清理 AI 生成内容 — Wikipedia’s Cleanup of AI-Generated Content。425/193（HN）。WikiProject 正在成规模清剿机器味条目。💬 一条评论把利害关系讲清楚了：Wikipedia 是训练语料，让它同时当模型输出会形成自噬循环；有人引用 MIT Tech Review 去年关于小语种维基被 AI 内容污染的报道，接着出现今日最佳比喻——「LLM 之前的存档，正在变成新的低本底钢」。还有人顺势指出 AI 实验室收购并销毁实体书的行为，与这个逻辑同源。
  • Anthropic 用盗版书训练 Claude 的判决 — Anthropic trained Claude on illegally obtained Stanford professors’ books。404/229（HN）。Bartz v. Anthropic 里 Alsup 法官划了两条线：合法购书训练算合理使用，用盗版书建永久中央库不行，最终 15 亿美元和解覆盖近 50 万件登记作品；斯坦福受影响的 10 位教授（包括国家艺术勋章得主 Tobias Wolff）认为和解远远不够。💬 评论区的高票是同一个类比：「按这个标准，Aaron Swartz 该被起诉 13 项重罪，而 Anthropic 只是民事和解。」争论焦点随即转到 Swartz 当年是否构成入侵，双方都在翻法庭文件。
  • Amazon 拆解 AI 部门 — Amazon Is Gutting Its AI Division After Sustained Failure。194/99（HN）。Futurism 七月的报道今天被重新翻上来，Nova 系列在内部评估里持续落后，部门被拆分重编。资源堆得最厚的一家交不出对标产品，这比任何评测榜都说明问题。
  • Liquid AI 发布 LFM3 — Introducing LFM3: Every Modality for Specialized Intelligence。101/36（HN）。主打「小而专」，多模态覆盖但把定位压在终端与专用场景，经营的是参数效率而非榜单。
  • Anthropic 与 Claude 加速药物研发的进展 — Early progress on accelerating drug development with Claude。70/55（HN）。实验室合作的中期报告，价值在于给出了具体的化学/生物环节耗时对比，而不是「AI 能加速科学」这类空话。
  • 当 agent 干活时，人还需要知道什么 — Here be monsters: What do you still need to know when agents do the work?。140/72（HN）。作者把「能力退化」这个老话题落到了具体清单上：agent 代劳之后，哪些判断还得自己留着。
  • Survival LLM：离线生存知识库 — Survival LLM: AI assistant and emergency library that runs on your own computer。120/77（HN）。本地运行的应急知识助手，卖点是断网可用——模型能力在这种场景里排在体积和可靠性之后。
  • Hex 融资 1 亿美元 — Hex Raises $100M。20/9（HN）。数据分析协作平台拿了新一轮，公告里更多在讲 agent 化的产品方向。
  • 评论里几乎没人提可靠性，业主提的频率是两倍 — Reviewers rarely talk about reliability. Owners bring it up twice as often。8/6（HN）。评测博客的措辞与真实使用者的关注点系统性错位，这个偏差本身就是对「评测驱动选型」的一记提醒。

🐍 语言与运行时

  • Python 的实验性 JIT 将被移除 — Python’s experimental JIT to be removed。418/220（HN）；85/17（Lobsters）。JIT 2024 年随 3.13 进入 CPython，当初只挂了一份 Informational 的 PEP 744；指导委员会 6 月要求补一份标准提案并给了六个月窗口，PEP 836 讨论数月后由维护者撤回，结论是代码退回主干之外。💬 争议集中在一个问题上：性能优化要不要走立法程序。一方说「你等于在要求一份『给 Python 换个解释器』的 PEP」，另一方翻出 HotSpot 与 Valhalla 的 JEP 反驳「大改动从来都要立项」；Lobsters 那边更尖，有人读完全程后认定这是「指导委员会在项目起势时用文书工作耗死志愿者」，也有人提醒便利的事实——JIT 的宏观基准收益本来就配不上它的维护面。顺带还留下了 Cython 与 CPython 混用的名场面。
  • 四个月 Zig — Four Months of Zig。45/19（HN）；23/5（Lobsters）。一份使用体验记录，重点在显式分配器与编译期执行带来的心智负担到底值不值。
  • OpenLDK：把 Java 世界搬进 Common Lisp — OpenLDK: Bringing the Java World into Common Lisp。81/8（HN）。在 Lisp 里实现 JVM 语义，动机是复用 Lisp 的交互式开发循环去调 Java 代码——罕见的、讲得清动机的语言桥项目。
  • Dioxus 全栈生产环境一年 — One year of Dioxus fullstack in production: the good, the painful。16/9（HN）。Rust 全栈框架的长周期实战复盘，好处和坑都具体到构件。
  • Debian 上的 Fil-C 二进制 — Filian, Fil-C binaries on Debian。15/1（Lobsters）。djb 记录把 Fil-C（内存安全 C 方言）编译的二进制搬进 Debian 的过程，这类工作通常没人写，但它是安全 C 能不能落地的前置条件。
  • Java 里的 Haskell 式类型类解析 — Full Haskell-like Type Class resolution in Java。11/1（Lobsters）。用 Java 的类型系统硬凑出类型类解析，属于「能不能做」压过「该不该做」的那一类。
  • 有符号 64 位常量除法的更快算法 — A faster way to compute signed 64-bit floor division by constants。44/7（Lobsters）。编译器后端常做这件事，作者把有符号情形的取整方向陷阱和修法写全了。
  • 编译期依赖类型 — Compile-Time Dependent Types。17/5（Lobsters）。Syl 的入门材料，演示依赖类型在编译期能消掉哪些运行时检查。
  • Theseus：玩具级的 bit provenance 抽象域 — The Shift of Theseus — Toy Bit Provenance Abstract Domain。2/1（Lobsters）。追踪整型里哪些位参与过哪些运算，PyPy 博客的小实验，读它是为了理解抽象域怎么设计。

🛠️ 工具与基础设施

  • Ghostty 1.4 — Ghostty 1.4。626/194（HN）；4/0（Lobsters）。💬 作者本人在帖子里把重点从 GUI 挪到了 libghostty：可嵌入的终端仿真内核，KDE 开发者回帖确认正在用它做一个新前端，并会提供 konsolepart 的替代实现；前 Neovim 核心开发者则表示「这事我 2019 年就想做，只是没人做」。这类项目的真正产出是一份可复用的终端仿真内核：长尾兼容性不再由每家公司各写一遍。
  • Tailscale SSH 的漏洞调查与修复公告 — Tailscale SSH: Investigation and remediation update。141/87（HN）。官方承认多数问题属于权限提升：已被授权通过 Tailscale SSH 连接的人，在某些配置下可以超出其本地用户的权限范围，补丁版客户端原计划 10 月 27 日发布；同时明确不建议所有人立刻关掉 Tailscale SSH。
  • Gram 3.4.0 发布 — Gram 3.4.0 released。71/11（Lobsters）。💬 评论区是罕见的「维护者与贡献者面对面」：一位贡献者交出了远程服务器二进制一键安装、以及用 postcard 替换 protobuf 的协议重写；维护者 mort 直接说扩展系统会走 Lua，已经有能跑通 LSP 命令的实验分支。小项目那种「我的提交真的算数」的感觉，被两个人几句话讲完了。
  • Rust 生态里的快速安全 tar 解析器 — A fast and secure tar parser for the Rust ecosystem。35/7（Lobsters）。Astral 给 tar 做的独立编解码实现，重点是拒绝畸形输入而不是跑分。
  • Stalwart v1.0 — Stalwart v1.0: The Fastest Mail Server on the Planet。38/18（Lobsters）。Rust 写的邮件服务器做到 1.0，自建邮件的门槛又被压低一格。
  • 为什么发一封邮件这么贵 — Why is it so expensive to send an email?。63/47（Lobsters）。把 SMTP 生态里反垃圾、信誉、退信处理那一整层成本拆开算账，读完会理解为什么「自建邮件」从来不是一台机器的事。
  • CSS-Tricks 换了新主人 — CSS-Tricks has a new owner。106/2（Lobsters）。Geoff Graham 从 DigitalOcean 手里把站点买回独立运营。2022 年卖给 DO 之后原创节奏肉眼可见地慢下来，这次是反向操作。💬 一条评论顺手补了同类案例：Waterfox 也被原开发者从私募手里买回过。
  • 网站应该能被打印 — Websites Should Be Printable。82/23（Lobsters）。💬 chrismorgan 写了本日最长的技术回复，逐条拆作者的 @media print 方案：浅色模式下行内代码会变成黑底黑字、代码块整块涂黑印出来、code { display: inline-block } 破坏行高、不要改链接颜色；他给出的判断更直接——「打印样式表的第一条规则，应该是别用打印样式表」。作者当场认了前两条并回帖感谢，JulianSildenLanglo 补上了自己站点的修法：a[href]:after { content: " [" attr(href) "] " }，让打印出来的 PDF 里链接地址可见。
  • Shitty Screenshare — Shitty Screenshare。73/31（Lobsters）。站点拿 OBS 直推 WHIP 与会议软件内建共享做画质对比，呼吁 WebRTC 会议应用把 WHIP 开放成输入源。💬 反驳也扎实：david_chisnall 指出观感差多半来自缩放与抗锯齿，与码率关系不大；有人举 Teams 对 Excel/PowerPoint 直接跑 Web 版的思路，喊「我一点都不想在开会被共享表格时本地启动一份 Excel」；也有人顺带确认 Discord 确实备了两套编码档位，文字档清晰但帧率低、鼠标轨迹会丢。
  • 一个 select 应该告诉你一些事 — A select should tell you something。8/0（Lobsters）。表单控件的可用性细节，讲到「空态该说什么、选中态该显示什么」这一层。
  • 用调用图分析器找出 panic — Finding panics with Call Graph Analyzer。9/0（Lobsters）。Rust 里定位「哪条调用路径会 panic」的静态分析实践，应急恢复逻辑值得抄。

🔒 安全与隐私

  • 美国政府藏着一份关于如何监控美国人的秘密法庭裁决 — US Government is hiding a secret court ruling about how it spies on Americans。710/257（HN）。Wired 报道一份被列为机密的 702 条款解释性裁决，多届政府都在依赖它。💬 最高票问的是概念问题——「法律的保密解释」凭什么成立？回答一层层剥下来：保密只有在泄露会危及具体人身或行动时才站得住，而「公布解释会证明这套监控违法」恰恰不属此列；另有国家安全法务视角的解释说明这类裁决为何容易被分类处理。NewJazz 的三段论也被顶上来了：既然存在秘密法庭和秘密搜查令，秘密法律解释就是自然的下一步。
  • Go 官方对 eMudhra 密钥泄露事件的回应 — Our Response To The eMudhra Key Disclosure Incident。19/7（Lobsters）。八个中间 CA 私钥泄露之后，Go 团队交代了证书链该怎么处置。昨天 Apple 那份公告（58/34，Lobsters）讲了另一半：macOS 平台会拦，但 curl 和 git 走 /etc/ssl/cert.pem，仍可能接受这批证书，得手动删根证书。
  • GoAhead 的三个 TLS 漏洞 — Three TLS Bugs in GoAhead。46/8（HN）。嵌入式 Web 服务器里挑后端顺带挑出的三个 TLS 实现问题，这类设备通常不会有人去更新固件。
  • 模糊测试器对 AI：Fuzzilli 与 BigSleep 在 JS 引擎上的比较 — Fuzzers vs. AI: Comparing Fuzzilli and BigSleep on JavaScript Engines。8/2（Lobsters）。Project Zero 把传统覆盖引导模糊测试和 LLM 找漏洞放在同一批目标上比，结论比宣传稿更有参考价值。
  • 《与 Berferd 共度一晚》（1992） — An Evening with Berferd: In Which a Cracker is Lured, Endured, and Studied (1992)。5/0（Lobsters）。入侵者诱捕与行为观察的经典论文，现在的蜜罐产业只是把它做成了产品。

🖥️ 硬件与科技公司

  • Apple 发布 M6 版 14 英寸 MacBook Pro — New 14-inch MacBook Pro with M6。245/294（HN）。硬件层面没有超出传闻的改动，讨论量集中在内存起步配置和价格上——293 条评论与 iMac 那条合起来，比规格表更能说明当前用户最在意什么。
  • Apple 更新 iMac（M6） — New iMac with M6。289/345（HN）。两条一起看：苹果把 M6 同时铺到笔记本与一体机，评论区关心的仍是内存配置起步价。
  • 树里露出 Raspberry Pi Zero 3W 与 Pi 4 Model A — Raspberry Pi Zero 3W and Pi 4 Model A spotted in device trees。54/17（HN）。内核 device tree 先于发布会泄题，型号命名暗示 Wi-Fi 模块与无网口的版本分化。
  • Micron 突然放弃 4F² DRAM，对手却在加倍投入 — Why Micron Is Suddenly Ditching 4F² DRAM as Rivals Double Down。127/19（HN）。存储工艺路线出现明显分歧，成本与良率之间的取舍被摆到了明面上。
  • Nvidia 与 Micron 占美国盈利增长的 34% — Nvidia and Micron Make Up 34% of America’s Earnings Boom。15/1（HN）。盈利集中度这个数字，与昨天 S-1 里的采购承诺表放在一起更好读。
  • Discord 将让任何人通过 Google 搜到公开服务器消息 — Discord will soon let anyone find public server messages through Google。181/109（HN）。只针对被设置为「可发现」的服务器，但对一个默认私密感极强的社区产品来说，索引化的连带效应很难只停在公开频道。

🎮 轻度与其他

📌 今日总结

今天的情绪是「验收」而不是「庆祝」：一份否决指数时间假设的论文，昨天靠热搜获得关注，今天靠 Lean 仓库、复现命令和 sorry 警告数量获得可检验性，Anthropic 与 OpenAI 在这条线上罕见地互相补位，而社区最冷静的声音（Impagliazzo 的原话、星系算法提醒）恰好也都在场。三条必读按顺序：ETH 论文与 formal-math/eth 的 Lean 工程一起看，这是 LLM 参与基础数学的方式第一次给出可复现的接口；LWN 的 Python JIT 移除与 Ghostty 1.4 对照看，能看清「长期维护承诺」正在成为基础设施项目的硬门槛；@media print 那条时长两年的评论串（chrismorgan 逐条拆解 + 作者当场回应）是今天少有的一手工程对话，比任何教程都实用。横向信号只有一个：同一周里，一家 AI 实验室靠形式化验证拿分，一个语言社区靠撤回提案守住工程标准——两件事都在说，现在被追问的不再是产品能做什么，而是谁愿意长期负责。