导语： 你订阅了 Claude Code、Cursor、Codex，却说不清这个月额度还剩多少；让 AI 写了一个月代码，到底省了钱还是烧了钱，没人对过账。这轮海外新货分两派：两件帮你把 AI 订阅的糊涂账算清楚，两件让你看清 AI 能力的真实天花板——一件把流体力学结果写成机器可检验的证明，一件干脆把整支 AI 制作 MV 的工程源码全部开源。全是近三十天内冒头的新项目，星标曲线都在往上走。
仓库： https://github.com/vinzdg/codenotch
先说大多数重度用户的真实处境：Claude 订阅一个、Cursor 一个、Codex 可能还有一份，外加谷歌的 Antigravity。每家的用量面板藏在不同的网页里，等你干活干到一半被「额度用尽」打断，才知道今天又超了。
codenotch 是一个 macOS 应用，干的事很简单：把 Claude Code、Cursor、Codex、Antigravity 这几家的用量限制，以一条 HUD 的形式钉在屏幕边缘，随时瞟一眼就知道各家还剩多少。仓库描述原文写的是 "pins usage limits from Claude Code, Cursor, Codex, and Antigravity to a screen edge"，一个功能，做到极致。
操作路径： 1. 打开仓库页面，按 README 的安装指引获取 macOS 应用（开源项目，免费，许可证以仓库为准）； 2. 授权它读取各家工具的本地用量数据； 3. 把 HUD 拖到你写代码时余光能扫到的屏幕边缘； 4. 从此续费决策从「感觉还够用」变成「看数字说话」。
和国内的差异： 国内的编码助手（通义灵码、腾讯 CodeBuddy、文心快码等）额度大多显示在自家插件内部，互相不通气，更没有一个跨工具的聚合面板。而国内开发者同时用两三家海外订阅的越来越多，这个「用量聚合」的生态位，海外刚刚有人补上，国内还是空白。
适合谁： 同时订了两家以上 AI 编码工具、每月订阅费加起来超过一顿火锅的人。
仓库： https://github.com/damejan80/tokentab
第二个工具和第一个是一对。codenotch 看「还剩多少」，tokentab 回答「花了多少」。
它是一个 CLI 工具，读取 Claude Code、Codex、Gemini CLI 这三个命令行工具留在本地的会话日志，把 token 用量折算成钱，算出你的 AI 编程成本。仓库描述的措辞是 "works out how much they cost"——注意是「估算」，各模型的单价折算口径以它 README 为准，但方向很清楚：把会话级的糊涂账，变成项目级的明白账。
为什么这件事值得单独说： 我见过太多人一方面喊「AI 提效」，另一方面从不核算成本。一个替换掉的外包工作量值多少钱？一个花了三倍 token 还没调通的坑值多少钱？没有账本，这些全靠感觉。tokentab 这类工具的意义不是省钱，是让你第一次有能力做「AI 投入产出」的决策。
算账的完整链路长这样：
flowchart TD
A[三个CLI的本地会话日志] --> B[tokentab 解析日志]
B --> C[统计每次会话Token用量]
C --> D[按模型单价折算金额]
D --> E[按项目和日期汇总]
E --> F[终端里出报表]
G[codenotch 常驻屏幕边缘] --> H[读取各家订阅剩余额度]
H --> I[剩余量HUD实时显示]
F --> J[砍哪个留哪个有依据]
I --> J
操作路径： 1. 找到各 CLI 的本地会话日志目录（具体路径见 README，Claude Code 系的日志默认就在用户目录的配置文件夹里）； 2. 安装 tokentab 后对日志目录跑一次统计； 3. 按项目、按模型看分布，重点看「token 花得多但产出少」的那几个会话； 4. 每月固定跑一次，和订阅费对账。
和国内的差异： 国内个人开发者更习惯看 API 中转站后台的账单，或者团队层面架一个网关统计；但「会话级、项目级」的个人对账工具很少见。而且 tokentab 读的是本地日志，数据不出门，对在意隐私的用户友好。
适合谁： 用命令行 AI 工具干活的独立开发者；需要向老板或客户证明「AI 成本可控」的团队负责人。
仓库： https://github.com/openai/NavierStokesAndEuler
第三件换换脑子。OpenAI 在官方账号下开了一个仓库，名字直译过来是「纳维-斯托克斯与欧拉」，描述只有一句："Lean certificates accompanying Navier-Stokes and Euler results"——伴随其纳维-斯托克斯与欧拉方程相关研究结果产出的 Lean 证书。
翻译成人话：AI 在数学上给出的结论，不再只是聊天框里的一段「我证明了」，而是附上一份用 Lean 语言写成、可以被证明助手逐行机器检验的正式证明文件。具体证明了什么范围、推进到什么程度，README 是第一手信息，我不做超出描述的解读；但「把证明过程做成机器可检验的证书并公开」这个动作本身，就是 AI for Math 这条线上的标志性进展。
为什么普通开发者也该看一眼： 这代表一个范式——AI 的产出可以「附带可验证的凭据」。今天 Lean 用于数学证明，明天同样的思路就是代码的形式化验证、合同条款的机器核验。看得懂趋势的人，会提前想自己领域里什么是「可验证凭据」。
和国内的差异： Lean 社区国内参与者一直偏少，中文系统材料稀缺，这个仓库等于一份免费的真实案例教材——所有证明都是机器检验过的，比任何教程里的玩具例子都有含金量。
适合谁： 数学系学生、对形式化验证感兴趣的工程师、想往 AI for Math 方向靠的研究者。
仓库： https://github.com/JohnHeibel/PDoomVideo
「P(doom)」是 AI 圈的老黑话，指「AI 引发灾难的概率」，这首歌的标题本身就是个圈内梗——把一个严肃话题做成一支 MV，这很极客。
为什么值得点进去？看的不是成片，是工程文件。 国内 AI 视频工具（即梦、可灵、Vidu）出片确实快，但你拿到手的只有一段成片，提示词、分镜、剪辑工程全在作者肚子里。而 PDoomVideo 把整条链路的源码摊开——相当于一份「AI 做一支 MV」的公开教案，从歌词可视化到画面生成的每一步都可以拆开研究、改改就用。
和国内的差异： 国内的 AI 视频生态强在「出片效率」，弱在「工程可复刻」。想要的效果换个工具就复现不出来，是多数创作者的共同体验。海外这种「连源码一起送」的玩法，才是真正可以抄的作业。
适合谁： 短视频创作者、AI 视频玩家、想研究「AI 完整作品是怎么被工程化生产出来」的人。
一句话收尾：工具的下半场，比的不是谁生成的更多，而是谁算得更清、验证得更严。账本和证书，就是 2026 年秋天最被低估的两样东西。
本文由「51学通信」技术团队出品。51学通信由通信行业18年老兵爱卫生（微信ID: gprshome201101）维护。 聚焦5G/6G核心网、3GPP标准、AI工具实战。知识星球「51学通信」提供深度技术答疑和行业洞察。
[!tip] 51学通信知识星球 星主：爱卫生（微信：gprshome201101）——公众号「51学通信」创办者，19 年通信行业运维与讲师经验，著有《GPRS网络信令实例详解》《EPC原理与实践》《5G核心网原理与实践》三本纸质书（各大电商平台有售）。 星球定位：深耕 5G 核心网、IMS、NFV/AI、云原生等 ICT 领域，主打运维岗位与信令分析。 当前规模：5200 篇主题 / 990 个回答，198 元/年。 加入福利：加入星球后请加爱卫生微信，拉您进知识星球年度陪伴与答疑群——不限量回复您的各种问题，另有群内分享。 AI 加持：51学通信知识星球已作为 skill 接入 WorkBuddy，使用 deepseek-4-flash 在海量星球帖子中精准找贴、找视频、找 FAQ 和案例，做总结、找文档和 PPT 等场景全覆盖。