lpviz 是一个交互式线性规划可视化工具，需要 JavaScript。同时，文档无需 JavaScript 即可使用：lpviz 文档 · 单纯形法 · 内点法 · PDHG · 椭球法 · 中心路径
每日HackerNews RSS
Hacker News 讨论介绍了 lpviz.net，一个用于可视化线性规划算法的交互式浏览器工具。用户可以绘制可行域并设置目标箭头；工具展示 Simplex、对偶 Simplex 等求解器如何找到最优顶点。创作者表示其目标是建立对求解器行为的直觉，补充专注于建模的课程。评论者称赞它并要求更多透明度，如逐步更新和 LaTeX 计算；创作者建议可能加入单独的逐步模式，并提到 3 变量版本正在开发中。另一位评论者解释了 LP 基础：约束定义可行域，目标优化线性函数，最优解常出现在顶点。此外还讨论了退化以及 active-set/criss-cross 方法，有一个分支加入了 criss-cross 和 proximal primal-dual active set。帖子包含网站链接和 YC 广告。
请启用JavaScript并禁用广告拦截器
黑客新闻
最新 | 过去 | 评论 | 提问 | 展示 | 工作 | 提交
登录
通过沿着父亲的足迹攀登来处理他的去世
（nytimes.com）
11 分，由 elemeno 发布于 1 天前
隐藏 | 过去 | 收藏 | 讨论
帮助
考虑申请 YC 2027 冬季批次！申请开放至 11 月 2 日。
指南 | 常见问题 | 列表 | API | 安全 | 法律 | 申请 YC | 联系
搜索：
作者需要一个无分支公式来提取浮点数中的最低置位。无法手动找到，他们对一组精选常量上的最多五次运算表达式进行暴力搜索，并用归纳搜索剪枝重复输出。这找到了几个五运算公式；其中一个可复用公共子表达式，减少到四次运算。最终表达式计算 a = x 的指数/符号位，然后以浮点数形式返回 (x 的位与 (a - x 的位)) 减 a。它通过翻转符号位处理 2 的幂，这对作者的 FPU 模拟器可接受。搜索约四分钟，证明穷举枚举可以发现不明显的位操作优化。
Hacker News 线程链接到一篇关于对 FPU 模拟器进行超级优化的文章。作者解释说，对于位计数操作，使用浮点减法是因为基于 ctz 的整数方法需要复杂处理次正规数和 2 的幂，且更难向量化；浮点减法在现代硬件上更快，并且适合 WASM。评论者讨论隐藏的浮点到整数转换、CTZ/CLZ 与 FSUB 之间的 ISA 权衡，以及一个玩具超级优化器。一位评论者指出，对每种组合进行微基准测试不切实际，另一位则批评 AI 时代的博文写法。总体来说，该线程涵盖底层优化权衡和模拟器设计。
Lean v4.35.0 在 AI 发现内核漏洞后加强了证明检查。`lake check` 在沙箱中导出并用 leanchecker 重新检查开发内容；`lake check --paranoid` 还运行 nanoda、lean4lean、con-leche、con-ron，以及一个加固内存分配器的内核变体。Con-leche 是首个用 Lean 编写并证明一致的 Lean 内核；它能快速检查 Mathlib，但编译器/运行时缺陷仍可能发生。Con-ron 是一个被验证为细化 con-leche 的 Rust 版本，因此同时使用两者可降低共享编译器/运行时风险。Lean4lean 的验证预计很快完成。开发者也在翻新内核、构建更简单的内核，并为大型项目规划二进制/增量检查。用户被敦促运行 `lake check --paranoid` 并报告内核分歧。
关于 Lean 发布经验证内核（Lean 中的 con-leche、Rust 中的 con-ron，部分由 Claude 构建）的 Hacker News 讨论。评论者争论近期数学突破来自 LLM 加 Lean 还是仅 Lean。共识是：Lean 负责形式化而非发现；LLM 提供创造力，Lean 的类型检查器提供正确性，二者迭代循环推动进展。人类很少先形式化再非形式化证明；LLM 先用自然语言推理，再翻译成 Lean。评论者指出形式化对人类繁琐且缓慢，数学家的挫败感针对 LLM 驱动的变革而非 Lean 本身。其他人讨论 Lean 的可读性、与 Agda/Coq 的比较，以及形式语言能否重塑数学教育。在验证方面，多个内核降低共享编译器/运行时错误的风险；哥德尔相关担忧被认为不切实际。一些人指出 Lean 作为通用编程语言和 DSL 载体的潜力。
请启用 JS 并禁用任何广告拦截器
Hacker News 的帖子讨论了 Meta 在抗议日短暂封禁 No Kings Instagram 账号一事。据报道该账号离线约 90 分钟，组织者表示管理员在额外数小时内被禁止发帖。评论者争论此次封禁是自动审核或举报滥用的误判，还是蓄意的政治压制。有人认为 Meta 过度依赖自动化，协同举报可以触发封禁；也有人认为其临时性表明并非有意去平台化。讨论还引发了更广泛担忧：私人平台控制政治言论、审核透明度、Meta 对其他政治账号的处理以及与其他平台的对比。部分评论者称没有证据表明存在政治动机，另一些人则指出 Meta 过去的模式及其与权势利益的关系。总体而言，该帖子聚焦于问责、平台权力以及依赖大型科技公司进行政治组织化的风险。
Vacuula 是一个一体化自定义服务器，用于修复和控制损坏的 Neato 机器人吸尘器。目前支持 Gen3 机型（D3–D7）和 Gen4 机型（D800、D8–D10），但不支持 Gen1（无 Wi-Fi）或 Gen2 BotVac Connected，后者计划支持。已完成功能包括设置/状态、地图、历史运行记录、调度、设置、区域/禁行线以及 Gen4 多区域；进行中的功能包括通知、Home Assistant 实体、拖拽清洁、自定义声音、体验改进、次日调度以及 Gen2/Gen3 多区域。处于“彩虹模式”的 Gen4 机器人可通过 Discord 获得维修帮助。服务器必须在专用硬件上持续运行，可通过 Home Assistant 或 Docker Compose 安装，并提供安装器来配置机器人。默认端口为 80（Web 应用/API）、443（Gen3）和 3443（Gen4）。已在 ARM64 和 x86-64 上测试，未来可能支持 32 位平台。
Hacker News 上题为“Custom server to revive neato bots”的帖子链接到 github.com/vacuula，有 63 点和 3 条评论。讨论包括逆向工程 Neato 激光雷达，以及 Gen3 机器人目前依赖 nip.io 和端口 443 的担忧。创建者表示 Vacuula 正在移除 nip.io 依赖，并在即将发布的 1.1.0-b1 版本中覆盖固件对端口 443 的依赖。
纽约宣布游戏所有权法案，要求拥有所有权而非许可 NY announces game ownership bill requiring ownership rather than licensing
2 天前
众议员里奇·托雷斯提出《玩家权利法案》，旨在通过指示联邦贸易委员会监管游戏所有权来保护玩家。该法案将授予消费者所购游戏的实际所有权，而非可撤销许可，并要求在服务器关闭前提供离线模式。它追随宾夕法尼亚州参议员约翰·凯恩的《保护我们的游戏法案》和“停止杀死游戏”运动。引用的例子包括育碧《The Crew》停服、《NBA 2K25》两年后下架，以及《守望先锋2》取代原版。索尼辩称购买的是许可，而非持久权利。该法案还可能涉及转让权，尤其是实体副本，但细节尚不清楚。倡导者说，盗版往往在无DRM的情况下提供更好的体验。该立法标志着终结游戏行业反消费者做法的重要一步。
Hacker News上的一篇帖子讨论了纽约州一位代表提出的一项联邦法案，该法案将要求视频游戏的所有权而非许可。评论者指出该法案仅已宣布，尚未正式提出，并对其通过机会提出疑问。讨论扩展到更广泛的版权改革、更短的版权期限、DRM限制、离线游玩、游戏保存和数字转售。一些人认为合理使用、更短的版权期限或源代码托管更能保存老游戏。其他人担心仅在线游戏、独立开发者负担、执法以及可能转向SaaS模式。支持者说支持离线、无DRM游玩是可行的，消费者应真正拥有购买内容，而批评者指出许可安排可以透明，数字转售可能扰乱市场。总体情绪混杂：对消费者所有权的兴趣很强，但对可行性、法案细节和实施仍持怀疑。
PNG 文件由块组成，每个块包含长度、类型、数据和 CRC。关键块包括 IHDR（图像元数据）、IDAT（压缩图像数据）和 IEND（结束标记）。解码时，拼接所有 IDAT 数据并用 zlib 解压，得到带滤波的扫描行。每行扫描行以一个滤波字节开头；反滤波将其还原以恢复像素。交错 PNG 使用 Adam7 存储七次逐步更详细的遍历。块名称编码块是关键/辅助、公开/私有，以及是否可安全复制。示例是一个 256×256 的真彩色 RGB 图像。
Hacker News 上的帖子讨论了一篇解释 PNG 每一步解码过程的文章。用户们辩论了 PNG 块元数据：关键块与辅助块、伽马/色彩空间的默认值、背景颜色，以及 IEND 尾块为什么是使文件自定界所必需的。评论者指出，许多查看器历史上忽略了物理尺寸，回退默认值仍然可能“足够正确”。其他评论分享了个人的 PNG 解码器项目和图形文件格式资源，还建议建立一个收集格式解码指南的网站。YC 申请页脚与此无关。
78岁的宾夕法尼亚大学退休教授卡罗琳·马文因在费城市中心人行道上反复拒绝警方要求，继续阻挡 Uber Eats 送餐机器人，而被以扰乱秩序罪逮捕。自这些机器人于3月推出以来，马文一直习惯站在它们前面，抗议企业用机器人取代人类送餐员。她计划以第一修正案为由抗辩该指控，并表示将继续抗议，将其视为公民参与和公民责任。她形容公众反应分化——有些人支持，有些人担心顾客——但认为机器人对送餐员的影响也应引起担忧。她小心不阻挡人类行人。此次事件是她持续数月抗议中警方首次介入。Uber 拒绝置评。
一名退休的宾大教授因反复阻挡 Uber Eats 送餐机器人而被费城警方逮捕，称其抗议企业取代人类工人。HN 评论者争论这是否是值得逮捕的正当公民不服从，还是非法阻塞公共人行道。有人认为第一修正案不保护干扰机器人配送；也有人认为机器人不应与行人共享人行道，或应给行人让路。讨论还涉及对紧急配送的可能影响、机器人在法律上被归类为行人的问题，以及自动化、公共空间和负外部性等更广泛关切。总体而言，该帖凸显了抗议权与商业机器人占用人行道之间的紧张关系。
JDK 28 JDK 28
3 天前
本版本将是 Java SE 平台第 28 版的参考实现，由 Java Community Process 中的 JSR 403 指定。状态：主线已开放，用于错误修复、小规模增强，以及通过 JEP 流程提议和跟踪的 JEP。在 GPL 下的早期访问二进制文件可在此处获取。特性。最后更新：2026/10/15 14:44 UTC。
Hacker News 上关于 JDK 28 的讨论涉及 Java 的加速演进及其在现代生态中的地位。评论者指出 Java 在过去 10–15 年持续改进，Java 8（lambda、stream）是转折点。Java 与 Kotlin 的争论持续：Kotlin 的类型系统和简洁性对比 Java 的运行时控制（虚拟线程）与框架生态（Spring、Quarkus）。在 AI 时代，Java 的冗长性不那么重要，而其快速、可扩展的运行时、深度遥测（JFR）以及 GC 选项（ZGC，几乎无停顿）是优势。Rust 对比出现：Java 常在复杂、长期运行的服务器应用中胜出，Rust 适合嵌入式和对冷启动敏感的工作负载，如 serverless。BEAM/Elixir 爱好者称赞其可观测性。JDK 28 的主要特性包括值对象（JEP 401）、结构化并发（JEP 543）、PEM 编码（JEP 542）和简单 JSON API（JEP 540），以及通过 AOT（JEP 544）和更快 ZGC（约 100ms）的启动改进。小型 Java 程序启动不到一秒；Spring 等重型框架会拖慢启动。Java 通过 Swing/AWT（内置）和 JavaFX（独立）支持 GUI。JSON API 的严格性（不支持尾随逗号/注释）引发了关于宽松与严格解析的争论。总体而言，Java 仍然是一个强劲且持续演进的平台。