2025 07 09 HackerNews

2025-07-09 Hacker News Top Stories #

超过400名媒体人士和BBC员工联名指控BBC董事会成员Robbie Gibb存在利益冲突，要求其辞职，认为其与犹太纪事报的联系可能影响报道公正性。

谷歌的虚拟助手Gemini将能够访问用户的WhatsApp消息，允许发送消息和回复通知，但用户可以通过关闭应用扩展或禁用Gemini来保护隐私。

数学家Boaz Klartag在球体填充问题上取得新进展，提出了在高维空间中高效填充球体的方法，解决了该领域的重大开放性问题。

一篇文章介绍了如何使用SVG格式实现类似GIF的动画效果，具有更小的文件大小和更高的分辨率，适合嵌入GitHub的README文件中。

OffChess是一款离线国际象棋谜题应用，提供超过10万个谜题，无广告、无订阅费用，支持一次性购买解锁更多功能。

文章指出Firefox浏览器的性能并未变差，但Mozilla的管理层被批评为缺乏方向感，导致错失多次机会，如裁掉Rust团队和放弃Servo引擎。

Hugging Face社区推出小型多语言长文本推理模型SmolLM3，性能优于同类模型，支持6种语言，能处理长达128k的文本，适合边缘/移动部署。

美国司法部威胁起诉开发反ICE应用的美国公民，认为该应用危及ICE官员安全，但开发者表示其目的是提供信息而非妨碍执法。

一篇文章介绍了在Lean 4.22版本中新引入的验证基础设施，用于证明命令式程序的性质，并展示了一个判断整数列表中是否存在两数之和为零的例子。

ProjectionLab创始人Kyle Nolan分享了如何将一个副项目发展为年收入超过100万美元的企业，强调坚持不懈和适时的市场验证是成功的关键。

Open letter accuses BBC board member of having a conflict of interest on Gaza #

https://www.theguardian.com/media/2025/jul/02/more-than-400-media-figures-urge-bbc-board-to-remove-robbie-gibb-over-gaza

超过 400 名明星和媒体人士，包括 Miriam Margolyes、Alexei Sayle、Juliet Stevenson 和 Mike Leigh，签署了一封致 BBC 管理层的信，要求撤换董事会成员 Robbie Gibb，因其涉及中东问题的潜在利益冲突。签署者还包括 111 名 BBC 记者和一些演员及历史学家，他们对 BBC 在报道以色列/巴勒斯坦问题时的编辑决策和审查表示“关注”。

这封信是在 Channel 4 即将播出 BBC 委托但搁置的纪录片《加沙：受攻击的医生》前夕送达的，BBC 称该纪录片“可能造成偏袒的印象”。信中指责 BBC“因担心被视为批评以色列政府而束手束脚”，并声称“不一致的指导方针应用方式使 Gibb 在 BBC 董事会和编辑标准委员会中的角色成为焦点”，因为“我们担心一个与犹太纪事报有密切联系的个人……在 BBC 的编辑决策中有任何发言权，包括决定不播出《加沙：医疗人员在火线》”。

Gibb 是特蕾莎·梅的前新闻主管，也是 BBC 威斯敏斯特政治团队的前负责人，他在 2020 年领导了一个财团购买了犹太纪事报，并直到 2024 年 8 月都是犹太纪事报媒体的董事。信中指出：“对我们许多人来说，我们在 BBC 高层做出的不透明决策让我们的努力受挫，没有讨论或解释。我们的失败影响了观众。作为一个组织，我们没有对英国政府在巴勒斯坦战争中的参与提供任何重大分析。我们未能报道武器销售或其法律含义。这些故事反而被 BBC 的竞争对手打破。”

声明声称 Gibb 有“利益冲突”，这“突显了 BBC 内容制作者的双重标准，他们自己因‘公正性’的名义而经历了审查。”信中还提到：“在某些情况下，员工因为在社交媒体上发布批评以色列政府的新闻文章而被指责有议程。相比之下，Gibb 仍然担任有影响力的职位，关于他的决策透明度很低，尽管他的思想倾向众所周知。我们不能再要求许可证持有者忽视 Gibb 的思想忠诚。”

信件总结道：“我们，签名的 BBC 员工、自由职业者和行业人士，对 BBC 对以色列和巴勒斯坦的报道继续达不到我们观众期望的标准感到极度担忧。我们认为 Robbie Gibb 在董事会和编辑标准委员会的角色是站不住脚的。我们呼吁 BBC 为我们的观众做得更好，重新承诺我们的公正、诚实和无畏无偏的报道价值观。”由于担心后果，111 名 BBC 记者匿名签署了这封信。

BBC 发言人表示：“我们编辑团队之间关于我们新闻报道的激烈讨论是编辑过程的重要组成部分。我们一直在讨论报道，并听取员工的反馈，我们认为这些对话最好在内部进行。关于我们对加沙的报道，BBC 致力于公正地报道冲突，并从该地区制作了有力的报道。除了突发新闻、持续分析和调查外，我们还制作了获奖纪录片，如《加沙：生与死》和《加沙 101》。”

HN 热度 505 points | 评论 315 comments | 作者：mhga | 22 hours ago #

https://news.ycombinator.com/item?id=44496391

BBC 作为公共服务广播公司，应该独立于政府，不受政治压力影响，自我审查不符合其宗旨。
以色列明显违反国际法时，欧洲政治家几乎不批评，美国则全力支持，BBC 不突出以色列负面行为是理性选择。
人们对 BBC 的行为感到愤怒和失望，但不感到惊讶，因为 BBC 的行为反映了更广泛的社会态度。
批评 BBC 的行为是合理的，即使 BBC 有其行为的理由，这并不影响对其行为的批评。
BBC 的行为是对社会外部约束的响应，这些约束是由接受以色列行为的社会塑造的。
一个由以色列律师撰写、由以色列赞助的报告被用来指责 BBC 对以色列有偏见，但该报告方法有缺陷，使用了 ChatGPT。
有关 BBC 对以色列有负面偏见的研究与解释相矛盾，但具体抗议活动的例子难以找到。
有关 BBC 偏见的报告并非学术研究，而是有倾向性的报告，不应被视为权威。

Google can now read your WhatsApp messages #

https://www.neowin.net/guides/google-can-now-read-your-whatsapp-messages-heres-how-to-stop-it/

这篇文章讨论了谷歌的新政策，即从 2025 年 7 月 7 日起，谷歌的虚拟助手 Gemini 将能够帮助用户在手机上使用电话、短信、WhatsApp 和实用工具，无论用户的 Gemini 应用活动是否开启。这意味着用户可以通过召唤 Gemini 并说出指令，例如“给[联系人]发送一条 WhatsApp 消息”，Gemini 就会执行这个操作。

然而，谷歌承诺在正常情况下，Gemini 不能读取或总结用户的 WhatsApp 消息。但是，如果通过谷歌助手或实用工具应用的帮助，Gemini 可能会查看用户的消息（包括图片），读取并回复用户的 WhatsApp 通知等。

谷歌发送的原始电子邮件引起了互联网用户的担忧，许多用户通过进入 Gemini 移动应用 > 个人资料 > 应用，关闭每个应用扩展来禁用连接的应用。对于那些想要完全禁用应用活动的用户，可以在 Gemini 移动应用中找到以下设置：Gemini> 个人资料 >Gemini 应用活动 > 关闭。关闭后，谷歌仍将保留用户数据长达 72 小时，以“维护 Gemini 应用的安全性”并允许 Gemini 进行上下文响应。

当 Ars Technica 的 Dan Goodin 联系谷歌询问是否有办法完全移除 Gemini 时，一位代表回避了这个问题，而是回应说，这个更新对用户是有益的：即使在关闭 Gemini 应用活动的情况下，用户现在也可以使用 Gemini 在移动设备上完成日常任务，如发送消息、发起电话通话和设置计时器。关闭 Gemini 应用活动后，用户的 Gemini 聊天不会被审查或用于改进我们的 AI 模型。

文章认为，谷歌不希望用户在 Android 手机上禁用 Gemini 是有道理的。像 Android、Chrome 和 YouTube 这样的平台是谷歌及其服务超越竞争对手的关键。它们是公司用来训练其宝贵 AI 模型的大量数据来源。

文章还提供了一种完全卸载设备上 Gemini 的方法，但这并不容易，需要一台笔记本电脑和一个名为 ADB（Android Debug Bridge）的实用工具。文章详细描述了如何下载 Platform Tools ZIP，解压 ZIP 文件，将文件夹添加到 PATH 以便全局运行 adb，以及如何在 Android 设备上启用 USB 调试。对于小米设备，还需要额外的步骤来启用 USB 调试。最后，文章指导用户如何通过 USB 连接手机，并在终端或命令提示符中输入命令来完全卸载 Gemini。

HN 热度 412 points | 评论 269 comments | 作者：bundie | 8 hours ago #

https://news.ycombinator.com/item?id=44501379

Google 从去年 11 月开始就致力于这项功能，但 Gemini 并不能读取 WhatsApp 消息
Gemini 只能发送消息和开始通话，不能读取消息或发送消息到群聊
如果智能助手不能与 WhatsApp 交互，对很多人来说基本无用
Google Assistant 连接到 WhatsApp 后，数据可能会流向 Google，但用户已经将 WhatsApp 与 Google 连接
Gemini 应该只能做其他任何随机应用在手机上能与 WhatsApp 做的事情
Google 不应滥用其作为操作系统来源的地位，给予其软件特权进入第三方应用
Gemini 不仅是一个应用，而是操作系统级别的功能，操作系统可以访问任何第三方应用
Apple Intelligence 也进行了类似的营销，但没有引起争议
有人认为 Siri 应该是操作系统级别的功能，而 Gemini 不应该
有人认为 Google 和 Apple 都在模糊界限，但司法部门不同意这些说法
有人认为 Google 为了方便而模糊界限，但其他人并不这么看
有人认为 Google 可能只是需要访问加密消息以提供更好的用户体验
有人认为不应该假设 Google 总是最大限度地滥用数据，尽管有可能
有人认为 Google 是一个广告公司，而 Apple 是一个消费者硬件公司，因此更信任 Apple
有人认为 Apple 也是一个广告公司，为 Apple 带来数十亿收入
有人认为 Google 和 Apple 都销售硬件和广告，很难说“就是那么简单”
有人认为讨论这个问题是基于大科技公司涉足多个领域的假设
有人认为“Apple 是一个硬件公司”的说法是一个陷阱
有人认为 Google 和 Apple 都控制着大量设备、数据、软件和用户，并从中获利

New sphere-packing record stems from an unexpected source #

https://www.quantamagazine.org/new-sphere-packing-record-stems-from-an-unexpected-source-20250707/

这篇文章讲述了数学家 Boaz Klartag 在球体填充问题上取得的新进展。球体填充问题是一个古老的数学问题，它探讨的是如何在高维空间中尽可能高效地填充球体。这个问题不仅在数学上具有挑战性，而且在密码学、远程通信等领域有着重要的应用。

文章首先回顾了球体填充问题的历史，提到 17 世纪初物理学家约翰内斯·开普勒发现，通过将三维球体像杂货店中的橙子一样堆叠，可以填充大约 74% 的空间，并猜想这可能是最佳排列方式。然而，数学家们花了近 400 年的时间才证明这一点。

在更高维度的情况下，数学家们仍然不知道答案，除了在 8 维和 24 维这两个特殊的维度上。多年来，他们提出了更好的填充方法，但这些改进都是小幅度的，且相对罕见。

文章接着介绍了 Boaz Klartag 的工作，他在短短几个月内就解决了这个领域最大的开放性问题之一。作为一个新进入这个领域的研究者，Klartag 通过复兴一个几十年前被专家放弃的旧技术，实现了在所有任意高维度上都有效的球体填充方法。他的工作触及了关于高维最优填充的几个长期辩论，包括最优填充应该是有序的还是无序的，以及它们能有多紧密。

文章详细描述了 1905 年数学家赫尔曼·闵可夫斯基提出的一个直观方法，即从空间中的重复点阵列（称为晶格）开始，然后在每个点周围画一个球体。这样，寻找给定维度中最优球体填充的问题实际上就变成了寻找一个点排列尽可能高效的晶格的问题。在二维情况下，最优晶格是“六边形”的，产生的填充看起来像这样：

[图片]

1947 年，数学家克劳德·安布罗斯·罗杰斯提出了一个不同的视角。他建议从任何晶格开始，即使是一个次优的晶格。不是在每个点周围画一个球体，而是在一个点周围画一个椭圆形状，称为椭球体，使其表面触及但不超过晶格中的其他点。

罗杰斯提出了一个算法，使用这个椭球体作为起点来构建一个密集的球体填充。这种方法的优点是，你不需要从一个特别高效的晶格开始就能得到一个高效的球体填充。你只需要选择正确的椭球体。但这引入了一个新的复杂性。与完全由一个数字（其半径）定义的球体不同，椭球体由几个不同长度的轴定义。维度越高，你可以拉伸椭球体的方向就越多，你的起始椭球体看起来会有多少种选择。

Klartag，魏茨曼科学研究所的数学家，一直对晶格和球体填充感兴趣，只是从未有时间深入了解。他的工作领域是几何学，不是晶格理论，他通常研究凸形状——不向内突出的形状。这些形状涉及各种对称性，特别是在高维度上。Klartag 坚信这使它们成为极其强大的数学工具。凸形状，他认为，是被低估的数学工具。

去年 11 月，Klartag 完成了他通常研究领域的一个重大项目后，注意到他的日程异常清晰。他说：“我想，我 47 岁了，我一生都想研究晶格，如果我不现在做，那就永远不会发生。”他请朋友，特拉维夫大学的巴拉克·魏斯，指导他在这个新领域的工作。

魏斯与 Klartag 和其他一些人开始了一个小研讨会，研究文献。Klartag 的家庭作业包括仔细阅读闵可夫斯基和罗杰斯的球体填充食谱。

当他读到罗杰斯将椭球体转化为球体填充的技巧时，他想知道为什么数学家放弃了这种方法。椭球体是凸形状，所以 Klartag 知道许多复杂的方法来操纵它们。他还意识到罗杰斯使用的起始椭球体是直观但效率低下的。他所需要做的就是构建一个更好的椭球体——一个在边界触及晶格中的其他点之前包含更多空间的椭球体——他就能设定一个新的填充记录。

他从他熟悉的一种方法开始，根据随机过程沿着每个轴扩展和收缩椭球体的边界。每当边界扩展到足以触及晶格中的一个新点时，他就冻结椭球体在那个方向上的生长。这确保了该点永远不会落在椭球体内部。但形状继续在其他每个方向上膨胀，直到它遇到另一个点。通过这种方式，椭球体会以断断续续、犹豫不决的动作改变形状，逐渐……

HN 热度 405 points | 评论 204 comments | 作者：pseudolus | 1 day ago #

https://news.ycombinator.com/item?id=44493196

高维空间中填充球体的方法可以极大地提高填充效率，这展示了高维空间的奇异性。
在高维空间中，单位 n-球体的体积相对于其边界立方体的体积在 n 增加时会迅速减小。
高维空间中单位球体与边界立方体体积比值的关系是非单调的，且在 n=6 时达到最大。
随着维度的增加，超几何形状的体积越来越分散在其表面。
3Blue1Brown 的视频可以直观地展示这种违反直觉的结果。
在 2 和 3 维空间中，这种观点并不成立。
如果这种观点在 10 或 20 维空间中成立，其影响仍然非常重要。
向父母解释自己的工作是真实的存在困难，更不用说研究不向内突出的形状了。
解释工作时使用难以理解的术语可能会让父母感到无聊但印象深刻。
当遇到立即使用超专业术语与陌生人交流的人时，可能会对他们产生不信任感，或认为他们缺乏情商。
适度到非常聪明的人会欣赏将复杂事物简单解释的难度和实用性。
人们普遍欣赏能够简单解释复杂事物的能力。
在数学中，有时可以真正将一个主题的复杂性降低，使其易于大多数人理解，而不会牺牲真实性。
将此类对话视为一种协议，并在开始时进行协商。
有些人更喜欢简短且充满术语的回答，因为这给了他们澄清他们想要问什么的机会。
有些人认为不欣赏简单解释的人可能在数学/逻辑和社会/情感智能上都很低，但这种情况并不常见。

SVGs that feel like GIFs #

https://koaning.io/posts/svg-gifs/

这篇文章介绍了一种名为 SVG 动画的技术，它类似于 GIF 动画，但使用的是可缩放矢量图（SVG）格式。这种 SVG 动画不仅文件大小小（仅 49KB），而且具有极高的分辨率，非常适合在 GitHub 的 README.md 文件中使用。

文章指出，创建这些 SVG 动画需要使用两个工具：asciinema 和 svg-term-cli。首先，用户需要上传 asciinema 录制的终端会话，然后使用 svg-term-cli 将其下载为 SVG 文件，最终可以将这个文件直接拖放到 README 中。这种方法在作者的项目中被广泛应用。

作者分享了自己对 SVG 动画的惊讶，认为这种动画形式非常有趣，主要是因为 SVG 规范本身就支持动画功能。具体来说，SVG 中可以使用以下几个标签来实现动画效果：

<animate>：用于逐时间动画单个属性。
<animateTransform>：用于动画变换，如旋转、缩放和平移。
<animateMotion>：用于沿路径移动元素。

这些功能正是 svg-term-cli 工具所利用的，从而实现将终端输出转换为可视化的动态 SVG 效果。通过这种方式，用户可以以更生动有趣的形式展示信息。

HN 热度 364 points | 评论 97 comments | 作者：cantdutchthis | 15 hours ago #

https://news.ycombinator.com/item?id=44498133

SVG 能够实现许多令人印象深刻的效果，包括无需 JavaScript 的 Wikipedia 示例。
SVG 最初是作为 Shockwave/Flash Player 的开放竞争对手以及 PDA 的应用格式出现的。
SVG 支持完整的 JavaScript 和网络功能。
SVG 1.2 版本曾提出包括打开原始网络套接字的 API，但最终没有实现。
SWF 格式曾能够将游戏、视频、网站、信息图表、工具和聊天室打包进单一的二进制分发媒体文件。
Adobe 对 SWF 的管理不善导致了它成为互联网上最大的攻击面，最终被禁止。
Adobe 对 Flash 的支持不足，导致其成为安全问题的代名词，并且忽视了开发者。
Flash 的集成开发环境是其真正的力量所在，为开发者提供了强大的工具。
有些人认为 Flash 的消失是好事，因为它减少了广告业对互联网的侵入。

Show HN: OffChess – Offline chess puzzles app #

https://offchess.com

这个网页是关于一个名为 OffChess 的应用程序的介绍。OffChess 是一个可以在任何地方、任何时间、离线状态下进行的国际象棋游戏应用。以下是网页的详细中文摘要：

OffChess 应用特点：
- 提供超过 100,000 个离线国际象棋谜题，用户可以在一个精心构建的应用程序中享受游戏。
- 应用程序可以在 App Store 和 Play Store 下载。
评分谜题：
- OffChess 上的每个国际象棋谜题都有评分，用户根据自己和谜题的评分获得或失去积分。
跟踪统计数据：
- 用户可以通过跟踪关于解决谜题技能的统计数据来提高自己的国际象棋技能。
主题选择：
- 用户可以根据自己的喜好为棋盘选择颜色，应用程序提供了多种主题供用户选择，确保用户能找到自己喜欢的样式。
无需 Wi-Fi：
- OffChess 允许用户在没有 Wi-Fi 的情况下也能即时访问超过 100,000 个谜题，无论是在飞机上、通勤途中，还是想要避免分心的时候。

网页还包含了一些其他链接，如“首页”、“关于”、“隐私”和“联系”。最后，网页底部显示了版权信息，表明 OffChess 的版权归属于 2025 年。

HN 热度 289 points | 评论 111 comments | 作者：avadhesh18 | 15 hours ago #

https://news.ycombinator.com/item?id=44498296

OffChess 是一个包含超过 10 万个国际象棋谜题的 iPhone/Android 应用，完全离线且无广告。
用户可以根据类别解决谜题，并根据表现获得或失去积分，有一个轻量级评分系统。
应用无需账户、无追踪、无月订阅费用，也不需要互联网连接。
有用户提到 OffChess 的一次性支付（4.29 欧元）可以解锁超过每天 7 个谜题。
Lichess 提供了一个不错的替代方案，尽管它们的离线支持有限。
TacticMaster 在 F Droid 上提供免费且功能相似的应用。
CT-ART 4.0 被认为是黄金标准，虽然不是完全免费，但提供了一些非常有教育意义的功能。
有用户建议增加“预移动”功能，以帮助保持更有经验的用户的流动状态。
有用户反映有时候不清楚谜题的目标是什么，例如“Brilliant queen win ahead!”可能会引起误解。
开发者表示如果谜题中提到了具体的棋子名称，那么目标就是赢得那个棋子，而不是赢得游戏。
有用户建议默认关闭文字提示，因为它们会透露太多提示。
用户希望增加自动进入下一个谜题的功能，点击“下一个谜题”会显得繁琐。
有用户发现应用中的一个拼写错误：“Egnlish Opening”应为“English Opening”。
有用户在 Android 15 和 Nothing phone 2 上遇到菜单无法打开的问题，可能是界面布局问题。
开发者表示 OffChess 网站很快将提供测试版，并包含多项功能。
有用户不理解为什么 Lichess 限制离线下载到 50 个谜题。
Lichess 的整个谜题库（超过五百万的位置，包含解决方案和主题标签）可以以 CSV 格式下载。
有用户表示喜欢 Lichess 应用的离线功能，因为它可以在恢复互联网连接后更新排名。
有用户赞赏单人开发者、无广告、无订阅的软件，并愿意为此付费。
有用户询问为什么不同时提供一个网页版应用，特别是对于那些很少使用手机且在办公室可能会感到无聊的人。
开发者表示 OffChess 网站很快将提供测试版，并包含多项功能。
有用户推荐 Raymond Smullyan 的《阿拉伯骑士的国际象棋之谜》作为国际象棋谜题书籍。
有用户认为这个应用完全符合“本地优先软件”的目标，即创建用户友好的软件。
有用户询问开发者从何处获得 1000 个附加谜题，并建议对非衍生资产进行归属。
有用户希望看到类似的东西出现在 GNU/Linux 桌面上。

Firefox is fine. The people running it are not #

https://www.theregister.com/2025/07/08/firefox_isnt_dead/

这篇文章讨论了 Mozilla 及其浏览器 Firefox 的现状和问题。作者 Liam Proven 认为，尽管 Firefox 目前面临一些困境，但它仍然是一个比大多数替代品更好的选择。文章指出，Firefox 的性能并没有变慢，实际上根据 Phoronix 的基准测试，从 2023 年底到现在，Firefox 的速度一直在稳步提升。

文章批评了 Mozilla 的管理层面，认为他们似乎不理解什么对产品有效，以及用户最关心的部分。作者提到，Mozilla 错过了许多机会，比如在 2020 年裁掉了 Rust 语言团队，而 Rust 现在是最受欢迎的编程语言。同样在 2020 年，Mozilla 放弃了 Servo 浏览器引擎，而这个引擎在 Igalia 接手开发后显示出强劲的兴趣增长。

文章还提到，Mozilla 在广告领域的做法也令人费解。尽管 Mozilla 的大部分收入来自广告，但它没有选择收购或整合广告拦截器，反而收购了一家广告公司，并取消了不出售用户数据的承诺。

作者指出，Mozilla 的领导层缺乏方向感，这可能是因为它从未需要过盈利，因为它从未需要过盈利。Mozilla 的角色更像是在扮演一个企业，而不是真正的企业。文章最后提到，Mozilla 的问题不在于应用程序本身，用户仍然可以选择使用 Firefox 或其分支版本。

HN 热度 238 points | 评论 181 comments | 作者：LorenDB | 12 hours ago #

https://news.ycombinator.com/item?id=44499057

Mozilla 面临着既要独立于谷歌发展收入，又要不通过 Firefox 盈利等相互矛盾的要求。
一些批评认为 Mozilla 的 VPN 成本过高，或者 Mozilla 资金不足，这些都是没有根据的。
Mozilla 的 CEO 薪酬虽然超过 1% 的收入，但在软件行业并不算是过高。
有人认为 Mozilla 和维基百科基金会都在偏离它们的核心使命。
维基百科的运营成本并不高，且其使命不仅仅是运行维基百科，还包括社会责任。
维基百科通过不断请求捐款的广告可能误导用户，让人们认为维基百科迫切需要资金来维持运营。

Smollm3: Smol, multilingual, long-context reasoner LLM #

https://huggingface.co/blog/smollm3

这篇文章介绍了 Hugging Face 社区新推出的一款小型多语言、长文本推理模型——SmolLM3。以下是文章的详细中文摘要：

SmolLM3 模型简介： SmolLM3 是一款 3B 参数规模的模型，它在效率上具有优势，性能超越了 Llama-3.2-3B 和 Qwen2.5-3B，并且与更大的 4B 模型（如 Qwen3 和 Gemma3）竞争。该模型支持 6 种语言（英语、法语、西班牙语、德语、意大利语和葡萄牙语），并且能够处理长达 128k 的长文本，使用了 NoPE 技术和 YaRN。Hugging Face 提供了完整的工程蓝图，包括架构细节、数据混合比例，以及如何通过三阶段预训练方法逐步提升跨领域性能，以及构建混合推理模型的方法。

模型架构和训练细节： SmolLL3 采用了与 SmolLL2 相似的变换器解码器架构，并进行了一些关键的修改，以优化效率和长文本性能。这些修改包括：

Grouped Query Attention (GQA)：用 4 组分组查询注意力替换多头注意力，减少了推理过程中的 KV 缓存大小。
NoPE：从每 4 层中选择性移除旋转位置嵌入，提高了长文本性能，同时不影响短文本能力。
内部文档掩码：在训练中使用注意力掩码，确保同一训练序列中不同文档的标记不会相互关注。
训练稳定性：移除嵌入层的权重衰减，以提高训练稳定性。

训练配置： 使用全球批次大小为 2.36M 个标记，序列长度为 4096，学习率为 2e-4，使用 AdamW 优化器，权重衰减为 0.1，梯度裁剪为 1。使用 WSD（Warmup-Stable-Decay）调度器，预热步骤为 2000，最后 10% 的训练步骤线性衰减至 0。模型在 384 个 H100 GPU 上训练了 24 天。

数据混合和训练阶段： SmolLL3 采用三阶段训练策略，混合了网络、数学和代码数据，逐步提升性能。预训练包括以下阶段：

第一阶段：稳定阶段（0T 到 8T 标记），建立强大的通用能力。
第二阶段：稳定阶段（8T 到 10T 标记），引入更高质量的数学和代码数据集。
第三阶段：衰减阶段（10T 到 11.1T 标记），进一步增加数学和代码数据的比例。

中期训练： 中期训练包括长文本适应和推理适应，这些训练比主要预训练短，但仍然具有一定的通用性，旨在提高模型在这两个领域的性能。长文本训练在额外的 100B 标记上进行，分两个阶段扩展上下文窗口：首先是从 4k 扩展到 32k 上下文，然后是从 32k 扩展到 64k 上下文。

文章最后提到，SmolLL3 在中期训练后，模型在长文本和推理方面得到了进一步的改进。

HN 热度 201 points | 评论 36 comments | 作者：kashifr | 8 hours ago #

https://news.ycombinator.com/item?id=44501413

SmolLM3 在 3B 级别上达到了最先进的性能，并且是少数完全开放的模型之一，提供了完整的代码和复现方法。
训练一个这样的模型大约需要一百万美元的 GPU 时间（4000 个 GPU/24 天）。
该模型被认为是开源模型中的佼佼者，提供了详细的训练方法和数据混合比例。
核心网络数据集和其他数据集都是公开可用的。
SmolLM3 支持工具调用，并且其聊天模板包含了 XML 工具和 Python 工具两个不同的部分。
SmolLM3 是一个适合边缘/移动部署的模型，其在基准测试中的表现优于 gemma3-4b。
SmolLM3 的大小接近 Qwen3 的 75%，被认为是一个很好的模型。
SmolLM3 的 RL 算法看起来很有趣，有些人还在使用 OpenAI 的算法。
对于需要在浏览器和移动设备上运行小模型的企业来说，SmolLM3 是一个不错的选择。
小模型在知识方面表现不佳，尝试将知识训练到小模型中可能不是最佳选择。
有些人尝试使用 WebLLM 和 Weaviate 数据库，但对速度有所抱怨。
Gemma 3n 的“俄罗斯套娃”方法可能有助于添加特定领域的知识。
通常检索是快速的部分，可以考虑更便宜的检索方法，如 Bm25。
有些人尝试微调 Mistral 7B，但结果并不令人满意。
微调模型时，使用预训练数据集方法可能更好。
在 Android 上，由于 Java 压缩问题，不能传输超过 2GB 的文件，需要下载模型并将其复制到应用的文件夹中。
SmolLM3 模型相对容易微调。
SmolLM3 是一个“小的大型语言模型”，在大型语言模型的标准下是小的，在小型语言模型中是大的。

DOJ goes after US citizen for developing anti-ICE app #

https://appleinsider.com/articles/25/07/07/doj-goes-after-us-citizen-for-developing-anti-ice-app

这篇文章讨论了美国移民和海关执法局（ICE）的行动以及一款名为 ICEBlock 的 iPhone 应用程序所引发的争议。ICEBlock 是一款免费的应用程序，允许用户报告 ICE 官员的行踪，从而警告其他当地人避开某些区域。美国司法部长 Pam Bondi 公开威胁了这款应用的开发者，称“我们正在关注他，他最好小心点”。然而，这种威胁似乎没有法律依据，看起来是对言论自由的违宪攻击。开发者 Joshua Aaron 表示，他的应用是为了“提供信息，而不是妨碍执法”。

文章还提到，特朗普政府威胁要起诉 CNN，仅仅因为 CNN 报道了这款应用的存在。国土安全部长 Kristi Noem 表示，他们正在与司法部合作，看看是否可以起诉 CNN，因为他们认为 CNN 的行为是在“积极鼓励人们避开执法活动和行动”，并认为这是非法的。CNN 则回应称，报道应用程序的存在既不违法，也不意味着新闻机构对此表示支持。

特朗普政府认为这款应用会危及 ICE 官员的安全。白宫新闻秘书 Karoline Leavitt 表示，这款应用听起来像是在煽动对 ICE 官员的进一步暴力行为。Leavitt 提到，对 ICE 特工的暴力行为增加了 500%，但没有提供任何证据，也没有考虑到 ICE 特工行动的可见度增加了 500% 以上。特朗普政府暗示，这款应用和对洛杉矶 ICE 突袭的任何抵抗都是导致这种未经证实的暴力增加的原因，而不承认 ICE 官员的行为可能在引发公众反应方面有任何作用。

洛杉矶市长 Karen Bass 在 2025 年 6 月表示，最初政府表示突袭是为了寻找暴力罪犯和有逮捕令的人，但她质疑如何从毒品贩子到 Home Depot，再到人们的工作场所，这些地方的人们只是在努力谋生。文章最后提到，作者 William Gallagher 是一位苹果历史学家和高级编辑，拥有 30 年在 BBC 和 AppleInsider 讨论苹果技术的经验。

HN 热度 176 points | 评论 70 comments | 作者：ProAm | 21 hours ago #

https://news.ycombinator.com/item?id=44496458

DOJ 公开威胁一个美国公民，称要对他采取行动
该事件显示了美国在某些方面变得多么失常
该应用的开发者尚未被起诉
该事件可能不构成事先限制，因为缺乏明确的禁止行为
政府的言论暗示和法律行动威胁可能被视为事先限制
通过 App Store 发布应用可能导致开发者身份暴露，增加法律风险

My first verified imperative program #

https://markushimmel.de/blog/my-first-verified-imperative-program/

这篇文章是关于 Lean 4.22 版本中新引入的验证基础设施的预览，这个基础设施用于证明命令式程序的性质。文章通过一个简单的编程任务——给定一个整数列表，确定是否存在两个不同位置的整数相加等于零——来展示这个新功能，并与类似工具进行比较。

文章首先介绍了这个问题的简单解决方案，即使用两个嵌套循环遍历所有不同位置的整数对。但这种方法效率较低，因此作者提出了一种改进方法：遍历列表，同时使用集合数据结构存储已见过的所有元素。当遇到一个数 x 时，高效地检查是否之前见过-x。如果见过，答案为真；如果遍历完列表仍未找到，则答案为假。这种方法使用哈希集合时预期时间复杂度为 O(n)，使用二叉搜索树时最坏情况为 O(nlogn)。在 Lean 中，这两种数据结构分别被称为 Std.HashSet 和 Std.TreeSet。

文章接着讨论了 Lean 作为函数式编程语言，对命令式（有状态）编程的支持，包括在单个函数内（通过 do notation）和跨函数（通过 monad transformers）的支持。文章主要关注在单个函数内的命令式编程。

作者使用局部命令式编程，很容易地写出了基于集合的算法。代码示例中，Id 和 do 告诉 Lean 我们希望在“局部命令式”模式下工作，然后我们可以访问类似 Python 的语法，包括可变状态、for 循环和早期返回等命令式编程的特性。

文章进一步讨论了如何在 Lean 中证明局部命令式程序的性质。传统上，这在非常简单的情况下是困难的，因此如果对证明感兴趣，通常最简单的方法是以函数式风格编写程序，类似于在 Haskell 中的做法。Lean 4.22 预览了一个新的框架，称为 Std.Do，旨在使验证命令式编程（局部和全局）变得容易。

Std.Do 的基础是 Hoare 三元组的经典概念，这意味着关于命令式程序的断言总是以“如果 P 为真，并且我运行命令 C，那么 Q 为真”的形式存在。Hoare 三元组的好处在于它们是可组合的，大型程序将由许多可能操作全局状态或有其他副作用的小函数组成，Hoare 三元组允许声明可以轻松重用的性质，以证明使用较小程序的较大程序的性质。

文章最后通过一个交互式定理证明器的示例，展示了如何使用 Lean 的 Hoare 三元组语法来声明 pairsSumToZero 函数的正确性属性，并使用 Std.Do 提供的 mvcgen（Monadic Verification Condition Generator）工具来分析局部命令式程序并告诉我们需要做什么来证明三元组。作者提供了一个循环不变式的示例，并解释了如何将其翻译成 Lean 所需的形式。最后，作者提到 Lean 要求证明五个事项，包括循环不变式的保持、进入循环前的满足情况、早期返回时的属性等。

HN 热度 173 points | 评论 79 comments | 作者：TwoFx | 1 day ago #

https://news.ycombinator.com/item?id=44492986

算法在处理任意精度整数时有效，但在固定精度整数下可能会错误报告“false”，例如数组[INT_MIN, -1]。
在 C 语言中，如果数组中同时存在 INT_MIN 和其他负数，则程序行为未定义，因为会导致有符号整数溢出。
可以通过跳过 INT_MIN 元素来修复问题，因为 INT_MIN 的加性逆元不可能在数组中。
Rust 在默认设置下，如果输入切片中包含 isize::MIN，在调试构建中会 panic，在发布构建中如果有两个这样的值会错误返回 true。
正式验证的 C 语言中，算法会正确处理类型（跳过 INT_MIN），否则不会有证明。
即使花费了大量努力，证明系统可能没有考虑到一些广为人知的问题，导致简单的案例中证明失效。
证明在它被编写的语言（Lean）中是正确的，如果改变证明的上下文（公理），证明可能会失效。
在 SPARK/Ada 中，如果无法证明 low + high 不会溢出，它会阻止你，并且如果无法证明，它会让你停下来。
SPARK 最有趣的部分是所有运行时检查都是隐式、自动生成的，并且需要被证明。
Lean 4 实际上是一个元编程语言，像 Racket 一样，是一个用于编程、元编程和定理证明的统一语言。

Bootstrapping a side project into a profitable seven-figure business #

https://projectionlab.com/blog/we-reached-1m-arr-with-zero-funding

这篇文章是关于 ProjectionLab 的创始人 Kyle Nolan 分享如何将一个副项目发展成为一个年收入达到 100 万美元的盈利性企业的故事。以下是文章的详细中文摘要：

ProjectionLab 的发展历程： 文章首先提到，ProjectionLab 在四年内从零开始，达到了 100 万美元的年度循环收入（ARR）。这一切始于 2021 年，当时 Kyle Nolan 受到财务独立运动的启发，想要更好地规划自己的生活，但找不到合适的工具，于是开始自己构建。他没有想到这个副项目最终会帮助超过 10 万家庭规划他们的财务未来。

里程碑回顾： 文章接着回顾了 ProjectionLab 的一些关键里程碑，包括从 2021 年 5 月的 150 美元月循环收入（MRR）增长到 2025 年 6 月的 83.3K MRR。这些里程碑标志着 ProjectionLab 的成长，包括发布博客文章、在公共场合演讲、减少日常工作时间以专注于 ProjectionLab、辞去日常工作全职投入到 ProjectionLab 中。

情感背后的数字： Kyle Nolan 分享了从零到年收入百万美元的真实感受，这并不是一个平稳上升的过程，而更像是在经历情绪的起伏，如同在被熊攻击的同时乘坐多巴胺过山车。早期的平坦月份、收入下降、取消订阅的时刻都让他质疑一切，考虑是否应该专注于企业晋升或者尝试进入大型科技公司。但是，他逐渐学会了情感的高潮和低谷是创业的一部分，并且“不放弃”实际上是一种超能力。

不放弃： 文章强调，虽然有很多人比 Kyle 聪明，但成功更多地依赖于一致性和每天坚持不懈地出现。与喜欢的人一起工作可以让这种坚持变得更容易、更有回报。

从单人开发到真正的团队： 在最初的两年里，Kyle 在工作之余独自工作，几乎牺牲了所有的休息时间。但长期来看，他知道需要做出选择：是自己继续做所有事情并看着增长停滞，还是找到具有互补技能的人开始建立团队。他只是一个普通的工程师，没有市场营销经验，所以他决定与擅长增长和市场营销的人合作。Jon Kuipers 在要求任何回报之前，先投入工作并证明了自己的价值。当需要全职增长合作伙伴时，Kyle 没有考虑其他人。

建立团队： 文章还提到了团队增加了一些承包商，他们都是来自 ProjectionLab 用户社区的传奇人物，他们擅长处理客户喜欢询问的复杂财务问题，还负责主持一对一会议、创建教程视频等。虽然可以将客户成功外包以降低成本，但拥有一个快乐且参与度高的用户社区对 ProjectionLab 来说非常重要。

未来计划： 达到 100 万美元 ARR 只是开始，这还不包括非循环收入来源，如终身订阅和一对一培训课程，这些使得月收入通常比循环收入高出 20% 到 50%。ProjectionLab 将继续专注于制作人们喜欢使用的优秀产品，保持精简、自给自足，并与客户的利益保持一致，不追求 AI 炒作或不惜一切代价的增长。

给正在建设者的一条小建议： 一旦你验证了你的想法，就继续每天出现，让它变得更好。即使在分心、增长停滞或感觉无意义的时候。即使那个说你不是“真正的企业家”的声音在你脑海中响起。Kyle 也经常被这样的声音困扰。所以，做大多数人做不到的事情：每天实际出现，并证明它是错误的。你永远不知道哪一天会改变一切。

文章最后，Kyle 感谢所有多年来支持 ProjectionLab 的人，他们改变了他的生活，他每天都兴奋地为这些人继续建设。

HN 热度 169 points | 评论 35 comments | 作者：jonkuipers | 1 day ago #

https://news.ycombinator.com/item?id=44495428

坚持不懈和适时的市场验证是成功的关键。
营销比代码更重要，早期的营销活动如写博客、推广、维护 Discord 服务器和及时回复邮件对成功至关重要。
在收入下降时通过增加博客文章来进行市场推广是一种有效的策略。
低期望值是幸福生活的基石，首先为自己构建产品，当人们真正注册并支付时，会感到非常激励。
深切关心解决问题的方式可以带来工作质量的提升。
每天坚持不懈地出现可以带来意想不到的惊喜和奇妙的地方。
利润率从早期的 90% 下降到今年的 65%，因为正在努力重新投资于增长和团队建设。
有些公司虽然年收入增长迅速，但利润为零或远低于零，创始人最终却能获得丰厚回报。
许多创业者过于关注收入而非利润，这可能导致他们披露利润时感到尴尬。
寻找与业务匹配的增长营销人员是一个挑战。
从一开始就关注全球灵活性，以满足国际客户的需求。
产品验证可能不是一个大的时刻，而是许多小时刻的累积。
每天有新用户付费注册是产品验证的一种方式。
及时退出日常工作，更早地全身心投入创业可能会更好。
分享成功之路，但无法强迫他人从中学习。