最新

我是一名在大型科技公司工作了十年的资深软件工程师。现在的我对每天的朝九晚五工作感到厌倦，尤其是面对那些压倒性的工作要求和随机的优先级变化，这些都要求我在规定的工作时间之外继续工作。 在我二十多岁的时候，尤其是还没有家庭的时候，我可以做到这一点，但我意识到，最近我越来越难以管理一切，尤其是抚养家庭。我希望每天能和我的孩子们在一起，不想再过40小时以上的工作周。 我觉得一个可持续的工作节奏是每天工作3到4小时，去创造一些东西。我热爱创造，因此这总是让我感到兴奋，但我对工作中需要在组织间产生影响的人员方面并没有那么兴奋或感到挑战，尤其是作为大型科技公司的高级工程师。 无论如何，这些只是我思考已久的背景：我想辞掉我的大型科技工作，去做一些自己的事情，赚取足够的收入来维持生活并帮助抚养我的家庭。从财务上讲，我现在有一些缓冲，但还不足以完全实现财务自由，所以我需要一些收入来维持房贷、孩子的开销和生活方式。 我该从哪里开始？我应该探索哪些想法？如果你们中有人做过这样的事情，你们的经历是怎样的？

我特别感兴趣的是那些正在构建或购买六自由度机械臂和轨道的人，然后将它们与视觉系统、传感器和工具更换功能进行集成。 部署目标是车库或家庭“实用”房间，机器人将被安装在桌子上或天花板上，目的是进行硬件分类、洗衣或打包行李。 我感兴趣的协作机器人包括Universal Robots的UR5和UR10（如果你有充足的资金进行实验），或者是AR4级别的硬件，或者SO-101加上lerobot（如果你在进行大量制作）。

简而言之：我正在开发一个名为 OpenATP 的 Python 包 [1]，它为 Lean 中的自动定理证明提供了一个通用接口。在最新版本中，我添加了对 Leanstral 1.5 [2,3]、Grok 和 Kimi Code [4] 的支持。我惊讶地发现，Grok 的准确性与 Claude Code 和 Codex 竞争，同时在时间和成本上都更具优势。有关更多详细信息，请参见本文的其余部分和 OpenATP 文档 [5]。 自动定理证明器接受形式化的声明（如 Lean 中的证明助手），并尝试合成证明。毫无疑问，大型语言模型（LLMs）已成为这一任务的主流方法。许多人专门为定理证明微调了 LLM，例如 Mistral 的 Leanstral 1.5 模型。然而，最近的一些论文表明，通用的前沿模型在编码环境中与这些专用模型竞争，有时甚至超越它们 [6,7]。 在我自己的研究中，我成功地使用 Claude Code 和 Codex 作为自动定理证明器。随着最近几个月新模型和环境的发布，我对它们在准确性和时间/成本方面的比较产生了好奇。我在进行基准测试时遇到了两个主要问题： - 我需要根据订阅计划进行计费，以使其变得可负担。 - 编译 Lean 需要大量内存，我需要一种便宜的方法来远程并行运行多个独立的代理。 我创建了一个名为 OpenATP 的开源 Python 包 [1] 来解决这两个问题。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 --------------------------------- 证明器 准确率 时间 成本 t/o --------------------------------- 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 --------------------------------- 证明器 准确率 时间 成本 t/o --------------------------------- 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/j97c1kqg8n6w0st2hk3dcq7ynx87rngm) - 斯坦福兔子场景 [链接](https://www.fibertoy.dev/view/j971mkwktr7bsen3ybyxks08vh87pd1a) 正如你从最后一个示例中看到的，你也可以使用自己的3D模型。我还没有制作资产管理器，但如果你有在线的3D模型，技术上是可以导入的。如果有人开始使用这个应用程序，我会制作一个资产管理器。 我非常希望能收到任何反馈。我还将整个代码在线开源，链接在这里 [GitHub](https://github.com/NabilNYMansour/fibertoy)。

我开发了ROMbug Earth，这是一款Windows浏览器，可以显示您访问的网站背后的IP地址、主机、估计的网络位置以及第三方连接信息。<p>它还包括WebRTC、DNS和IPv6泄漏检查，并提供一个基于WireGuard的可选全设备VPN。浏览器和网络检测工具是免费的；VPN每月收费4.99美元，无需长期合同。<p>目标很简单：大多数浏览器只向您展示网页，而不显示其背后发生的网络活动。ROMbug Earth旨在使这些活动变得可见。<p>网站：rombugearth.com<p>我希望能收到关于这个概念、界面以及哪些网络信息最有用的反馈。