最新

我在大型科技公司工作了十年，是一名经验丰富的软件工程师。我现在的人生阶段，觉得朝九晚五的日常工作让我非常厌倦，尤其是那些要求你在下班时间之外工作的、繁重且优先级随时变动的任务。 我年轻的时候，还没有成家，可以应付这样的工作。但现在我意识到，最近我越来越难以兼顾一切，尤其是抚养家庭。我想每天花时间和孩子们在一起，不想再每周工作 40 多个小时了。 我觉得一个可持续的工作节奏是每天工作 3-4 小时，并在此过程中构建一些东西。我热爱创造，这总是让我充满热情，但我对工作中需要影响跨部门人员的方面并不那么兴奋/有挑战性，尤其是在大型科技公司担任高级工程师时。 总之，这一切都是为了说明我长期以来一直在思考的事情：辞去我在大型科技公司的工作，自己创业，建立一个能产生足够收入来维持生计和抚养家庭的事业。我的财务状况目前有一些积蓄，但还不足以完全实现 FIRE（财务独立，提前退休），所以我需要一些收入来支付房贷、孩子和生活开销。 我该从哪里开始？我应该探索哪些想法？如果有人经历过类似的情况，你们的体验是怎样的？

我特别感兴趣的是那些购买或制造六自由度机器人手臂和导轨，然后将其与视觉、传感器和工具更换系统集成的人。 部署目标是车库或家用的“公用”房间，机器人将安装在桌子上或天花板上，用途可能是分拣五金件、洗衣服或打包行李。 我感兴趣的协作机器人包括 Universal Robots 的 UR5、UR10（如果你资金充裕，可以大胆尝试），或者低至 AR4 级别的硬件，或者 SO-101 加上 lerobot（如果你动手能力很强）。

简而言之：我正在开发一个名为 OpenATP [1] 的 Python 包，它为编码代理提供了一个通用的接口，用于在 Lean 中进行自动定理证明。在最新版本中，我增加了对 Leanstral 1.5 [2,3]、Grok 和 Kimi Code [4] 的支持。令我惊讶的是，Grok 的准确性与 Claude Code 和 Codex 相当，但速度更快，成本却只有一小部分。有关更多详细信息，请参阅本文其余部分和 OpenATP 文档 [5]。 自动定理证明器接收形式化陈述（在 Lean 等证明助手中使用），并尝试合成证明。不出所料，大型语言模型 (LLM) 已成为这项任务的主流方法。许多人专门为定理证明微调了 LLM，例如 Mistral 的 Leanstral 1.5 模型。然而，最近的一些论文表明，在编码环境中使用的通用前沿模型与这些专用模型相比具有竞争力，有时甚至表现更优 [6,7]。 在我自己的研究中，我使用 Claude Code 和 Codex 作为自动定理证明器取得了很大成功。随着过去几个月新模型和编码环境的发布，我一直很好奇它们在准确性、时间和成本方面的比较。在尝试运行基准测试时，我遇到了两个主要问题： * 我需要通过订阅计划计费才能负担得起。 * 编译 Lean 需要大量内存，我需要一种廉价的方法来远程并行运行多个隔离的代理。 我创建了一个名为 OpenATP [1] 的开源 Python 包来解决这两个问题。OpenATP 会自动将代理的 CLI 凭据转发到 Docker 容器中，以便通过订阅计划计费，并提供 Modal 后端以远程并行运行多个代理（Modal 提供每月 30 美元的免费计算额度）。有关所有支持的证明器/编码环境以及如何为每个设置凭据的详细信息，请参阅 OpenATP 文档 [5]。 OpenATP 的最新版本增加了对 Leanstral 1.5、Grok 和 Kimi Code 的支持。我对 FATE-H 和 FATE-X 数据集 [8] 的一个子集进行了一些小型基准测试，以进行比较。Kimi Code 的订阅速率限制过于严格，无法将其包含在基准测试中。 在 FATE-H 上，Claude Code 和 Codex 的速度最快，每项证明约 10 分钟。它们的成本也显著更高。Aristotle [9] 是免费的，并且在两倍的时间内实现了完美的准确性。Leanstral 1.5 也是免费的，其时间和准确性与 Aristotle 相似（一次未命中是由于 60 分钟超时）。DeepSeek 非常便宜，但也是最慢的。它的速度大约是 Claude 的三倍，并且遇到了 3 次超时。 Grok 登场了！Grok 的准确性与 Claude Code 和 Codex 相当，但成本却只有一小部分，并且是实际运行时间最快的。在更具挑战性的 FATE-X 数据集上，这种差异更加明显。Grok 的速度比 Claude Code 和 Codex 快约 50%，成本便宜约 3 倍。在这些更具挑战性的问题上，最便宜的证明器开始真正遇到困难。DeepSeek 的速度比 Grok 慢 4 倍，并且遇到了 4 次超时。 FATE-H --------------------------------- 证明器 准确性 时间 成本 超时 --------------------------------- claude 10/10 9:50 $2.05 0 codex 9/10 10:00 $2.68 0 grok 10/10 8:46 $0.94 0 deepseek 7/10 28:21 $0.15 3 leanstral 9/10 23:00 免费 1 aristotle 10/10 19:39 免费 0 --------------------------------- FATE-X --------------------------------- 证明器 准确性 时间 成本 超时 --------------------------------- claude 8/9 15:43 $3.60 0 codex 9/9 14:27 $3.70 0 grok 9/9 10:42 $1.31 0 deepseek 3/9 41:48 $0.21 4 --------------------------------- [1] https://github.com/henryrobbins/open-atp [2] https://news.ycombinator.com/item?id=48780801 [3] https://mistral.ai/news/leanstral-1-5/ [4] https://news.ycombinator.com/item?id=48935342 [5] https://open-atp.henryrobbins.com [6] https://arxiv.org/abs/2601.14027 [7] https://arxiv.org/abs/2602.24273 [8] https://github.com/frenzymath/FATE [9] https://aristotle.harmonic.fun

大家好，大约两年前，我萌生了制作一种新型 Shadertoy 的想法，并收到了许多宝贵的建议。现在我终于有了一些空闲时间，可以分享我的成果了。 Fibertoy 本质上是 Shadertoy，但你可以同时编写 react-three-fiber 和 glsl 代码。它提供了一个 Three.js 环境，这意味着你既可以创建基本的 3D 场景，也可以创建着色器场景。 以下是我用它制作的一些场景示例： * 基础 Voronoi 场景 [https://www.fibertoy.dev/view/j978r67mc84yg2d36g3z5n2nqd8as16q](https://www.fibertoy.dev/view/j978r67mc84yg2d36g3z5n2nqd8as16q) * 锥体追踪示例 [https://www.fibertoy.dev/view/j97c1kqg8n6w0st2hk3dcq7ynx87rngm](https://www.fibertoy.dev/view/j97c1kqg8n6w0st2hk3dcq7ynx87rngm) * 斯坦福兔子场景 [https://www.fibertoy.dev/view/j971mkwktr7bsen3ybyxks08vh87pd1a](https://www.fibertoy.dev/view/j971mkwktr7bsen3ybyxks08vh87pd1a) 从最后一个例子可以看出，你也可以使用自己的 3D 模型。我还没有制作资产管理器，但如果你有一个在线的 3D 模型，理论上是可以导入的。如果大家开始使用这个应用，我会考虑制作一个资产管理器。 我非常希望收到大家的反馈。我的全部代码也在线开源：[https://github.com/NabilNYMansour/fibertoy](https://github.com/NabilNYMansour/fibertoy)

我构建了 ROMbug Earth，一款 Windows 浏览器，可以显示您访问网站背后的 IP 地址、主机、估算的网络位置以及第三方连接。 它还包含 WebRTC、DNS 和 IPv6 泄露检查，以及一个可选的、使用 WireGuard 的全设备 VPN。该浏览器和网络检测工具是免费的；VPN 每月收费 4.99 美元，无长期合同。 目标很简单：大多数浏览器只显示网页内容，而不显示其背后的网络活动。ROMbug Earth 的设计宗旨就是让这些活动可视化。 网站：rombugearth.com 我非常希望收到关于概念、界面以及哪些网络信息最有用的反馈。