今天的AI新闻流又被大模型跑分和Agent框架刷屏了，但我翻了9月18日的GitHub新品数据后，留下的是四个“不在风口上”的仓库：一个专门排中文红头文件，一个让AI摸到调试器，一个治你的额度焦虑，一个是OpenAI名下安静出现的数学证明仓库。它们没有融资公告、没有发布会，Star数从675到1995不等，但每个都精准补上了一个现有工具链的缺口——而且中文圈基本还没人写过教程。文中所有Star数取自系统2026-09-18抓取的GitHub API快照，细节以各仓库README为准。
是什么：仓库 mizzlelover/gongwen-gbt9704-skill，截至9月18日拿到675星。按仓库自述，这是一个中文公文排版Skill：按 GB/T 9704-2012 生成可编辑DOC。GB/T 9704-2012就是《党政机关公文格式》国家标准——红头怎么留、标题正文落款用什么字体字号、页边距留多少，全有死规定。写过材料的人都知道，内容半小时，排版折腾两小时，就是这个标准的“功劳”。
为什么值得关注：市面上的AI公文产品几乎全在卷“内容生成”——帮你写请示、写总结。但真正磨人的格式层，主流方案还是去模板站下载docx人肉替换。这个Skill把格式规则做成了Agent可调用的技能包，让Claude Code这类工具直接产出符合国标的可编辑文档，而不是一张不能改的图片或PDF。仓库描述里还有一句很务实的安全提醒：请勿上传企业禁止对外公开的文件，可在本地或企业内网部署大模型后使用——作者很清楚这个场景的用户是谁。
国内对比：WPS AI、讯飞智能写作都有“公文模式”，但它们是云端黑盒，格式细节不可控、涉密内容不敢碰。这个路线是把国标规则本地化、代码化，格式百分百可控。
价格：开源免费，商业授权细节以仓库LICENSE为准。
适用人群：体制内、国企、事业单位的笔杆子；给单位做办公自动化的开发者——把它接进内部工具，就是一个“材料排版岗”的自动化底座。
是什么：仓库 duty1g/x64dbg-mcp-server，Zig编写，1995星，是小而美榜单上分数最高的项目之一。x64dbg是Windows逆向圈人手一个的开源调试器，以往要人肉操作；这个项目是它的原生MCP插件，把调试器能力直接暴露给AI Agent。也就是说，Claude Code这类工具现在可以下断点、读内存、单步跟踪了。
为什么值得关注：逆向分析是最典型的“AI插不上手”领域——IDA、Ghidra、x64dbg全是重度交互的GUI工具，AI只能在你背后干着急。MCP协议改变的就是这一点：任何工具只要包一层MCP服务，就从“人用的软件”变成“Agent可调用的器官”。这个项目等于给AI装上了逆向工作台的第一个接口，动态调试的门槛被实打实拉低了。
国内对比：国内安全培训基本停留在“教你手用x64dbg”阶段，“Agent驱动调试器”这个组合的中文内容几乎空白。对做恶意样本分析、CTF的从业者，这是实打实的效率倍增器。必须强调：此类工具只应用于授权的安全测试、自有软件调试和合规研究。
价格：仓库未标注收费信息；x64dbg本体开源免费。
适用人群：安全研究员、恶意样本分析师、CTF选手、做二进制uat自动化的工程团队。
是什么：仓库 vinzdg/codenotch，Swift写的macOS应用，1975星。功能一句话：把 Claude Code、Cursor、Codex 和 Antigravity 的用量限额，钉在屏幕边缘实时显示。
为什么值得关注：2026年的AI编程用户都有同一种焦虑——额度是个黑盒。用着用着弹一个"limit reached"，你才知道这周白干了；想省着用，又不知道还剩多少。官方给的都是网页版仪表盘，查一次切一次窗口。这个应用把“还剩多少”变成屏幕上一条常驻的余量条，写码时余光就能看到。痛点极小，但痛感极普遍——这正是“小工具拿大Star”的典型配方。
国内对比：国内用户多用中转站和镜像服务，额度信息散落在各家网页里，没有统一的本地视图。这类“把平台状态钉到菜单栏”的桌面级整合，国内基本没人做。
价格：仓库未标注价格，分发方式以仓库页面为准。
适用人群：同时订了多个AI编程工具、靠额度吃饭的重度用户；管理团队订阅额度的Tech Lead。
是什么：GitHub官方OpenAI组织名下出现了新仓库 openai/NavierStokesAndEuler，Lean语言编写，1946星，自述为“配套纳维-斯托克斯与欧拉结果的Lean证书”。Lean是数学界用来做形式化证明的编程语言——证明要写成代码，由编译器验证每一步推理，机器不通过就不算数。
为什么值得关注：这个仓库的信号意义大于工具意义。“AI做数学”此前多是新闻里的“号称解出了X”，而Lean证书是可机器验证的——它把“AI的数学成果”从公关话术变成了可以编译检查的资产。当然要保持清醒：截至发稿，我没有看到配套论文或官方公告，证明的具体范围和含金量有待验证，这里只陈述仓库存在及其自述。但“OpenAI开始给数学成果配形式化证书”这个动作本身，值得每个关注AI边界的人盯一眼。
国内对比：形式化验证在国内更多是芯片、轨交等行业的工程话题，“AI+形式化数学”的大众讨论热度远低于海外HN和X上的白热化。会写Lean的人在国内极为稀缺，这可能是下一个“早期红利技能”。
价格：免费开源。
适用人群：数学背景想转型AI的研究者；关注AI for Science落地信号的人。
flowchart TD
A[9月18日冷门新品区] --> B[公文排版Skill]
A --> C[x64dbg MCP插件]
A --> D[codenotch额度条]
A --> E[OpenAI Lean证书]
B --> B1["补格式层缺口<br/>中文特供"]
C --> C1["补动态调试缺口<br/>AI摸到逆向台"]
D --> D1["补额度黑盒缺口<br/>余量常驻屏边"]
E --> E1["补可信度缺口<br/>证明可机器验证"]
| 你以为的 | 实际情况 |
|---|---|
| AI公文产品=帮你写内容 | 格式层才是刚需，国标排版Skill让Agent直接产出合规可编辑DOC |
| 逆向分析AI插不上手 | x64dbg包上MCP后，下断点读内存成了Agent可调用的动作 |
| 额度只能等弹窗提醒 | 菜单栏常驻余量条已是1995星级的需求 |
| AI数学成果只是新闻标题 | Lean证书让它变成可机器验证的资产，会Lean的人极度稀缺 |
gongwen-gbt9704-skill，按其README装进Claude Code的技能目录，先拿一份不涉密的红头文件试产出，用WPS打开验证格式后，再考虑接入单位内部流程。codenotch 仓库看安装方式，装完第一件事是把最常用的两个工具余量都钉上屏。openai 组织等配套论文；想入场的开发者，去搜Lean社区官方教程，两周能写出第一个机器验证证明。本文由「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 等场景全覆盖。