OpenAI 开源数学仓库引爆本周 GitHub
AI Skill 生态爆发，OpenAI 用 Lean 重注形式化数学
本周 GitHub 新建热门仓库合计约 27,000+ stars。OpenAI 的 Lean 数学仓库以 12,100 stars 一骑绝尘；AI Agent Skill 类项目（艺术动画、HTML 回答、应用克隆）密集上榜，加上 Rust 重写 Word/AutoCAD，反映出 Agent 技能化与 clean-room 重写两大趋势交汇。
本周 GitHub 最火的趋势是：AI Agent 的「Skill 化」正在从概念变成可复制的工程范式，而 OpenAI 用一个 Lean 仓库把形式化数学推到了聚光灯下。
openai/math 【本周最热】
⭐ 12,100 stars
OpenAI 开源的 math 仓库 用 Lean 语言编写，是本周唯一破万的项目，且领先第二名近一万 stars。Lean 是形式化证明语言，OpenAI 此举与其在数学推理方向的投入一脉相承——当模型能力逼近研究级数学，可机器验证的证明语料就成了关键基础设施。对做 AI for Math、形式化验证或 LLM 推理评测的团队，这是本周必看的第一手材料。适合直接 clone 阅读结构，观察 OpenAI 如何组织数学语料。
alchaincyf/huashu-art-motion
⭐ 2,445 stars
huashu-art-motion 是一个艺术动画 Skill：35 种艺术风格、9 种解说语法，用代码让静态画作动起来。它代表了 Skill 生态里「内容创作」这条线——不是让 Agent 写代码，而是让 Agent 产出可消费的视觉内容。与下面的 answer-me-with-html 相比，它瞄准的是自媒体和创作者场景。适合做短视频、知识科普的创作者直接套用。
QingYunA/answer-me-with-html
⭐ 2,324 stars
answer-me-with-html 让 Agent 用一页可读的 HTML 回答复杂问题，而不是倾倒一大段文本。这个项目有意思的地方在于它抓住了 LLM 输出的「可读性」问题：长答案在聊天窗口里几乎不可读，而 HTML 是天然的排版层。与 huashu-art-motion 同属 Skill 层，但更偏知识工作场景。适合需要向非技术同事交付分析结论的工程师和数据分析师。
facebookincubator/muse-gadget-sdk
⭐ 1,792 stars
Facebook 孵化器开源的 muse-gadget-sdk 是一个用 C 编写的构建 Muse gadget 的 SDK。大厂孵化器以 C 语言开源硬件/设备侧 SDK 并不常见，值得嵌入式和硬件开发者关注其 API 设计与构建链路。适合做设备开发的工程师评估是否可作为新项目的起点。
nullmoth/nvidia-macos-driver
⭐ 1,094 stars
nvidia-macos-driver 用 Rust 写了一个 Metal 驱动，让 NVIDIA RTX 显卡能在 macOS 15 Sequoia（Intel / OpenCore）上工作，免费且含源码。这是社区对「苹果放弃 NVIDIA 支持」这一被忽视需求的硬核回应。与商业驱动方案相比，它的价值在于完全开源可审计。适合手里有 RTX 卡和老 Intel Mac 的用户，但驱动类项目务必先备份系统再尝试。
Jakeschincariol/replica-skill
⭐ 1,083 stars
replica-skill 提供十一个免费 Claude Skill：逆向工程任意应用、重建、找 bug、再修掉用户最讨厌的问题，MIT 协议。它把「克隆一个产品」拆成了 Agent 可执行的流水线，是本周 Skill 生态里工程化程度最高的样本。适合想学习 Skill 编写范式的开发者逐个拆解其 prompt 结构。注意：克隆他人产品需自行评估法律边界。
storytold/wordcraft 与 cadcraft
⭐ 825 stars / ⭐ 763 stars
同一组织 storytold 一周内同时开源两个纯 Rust 的 clean-room 重写项目：wordcraft（重写 Word）和 cadcraft（重写 AutoCAD 风格 CAD）。办公与工业设计软件是被垄断最深的两个领域，用 Rust 从零重写既是技术宣言，也是对「桌面软件必须有巨头才能做」的挑战。适合 Rust 开发者参与贡献，或作为大型 Rust GUI 项目的学习样本。
mhtsec/ARTEX
⭐ 739 stars
ARTEX 是 AI 自主渗透测试系统，百度「agent+」攻防挑战赛冠军项目。它把 Agent 的自主规划能力用在了攻防场景——与前面所有「帮你做事」的 Skill 不同，这是「自主完成任务闭环」的极端测试场。适合安全团队评估 Agent 在红队场景的能力边界，仅限授权测试环境使用。
趋势雷达
把本周榜单放在一起看，三条线很清晰：其一，Agent Skill 成为新的开源品类，从动画、HTML 回答到应用克隆，Skill 正在像当年的 dotfiles 一样被标准化分享；其二，OpenAI 押注 Lean 形式化数学，暗示可验证输出是推理模型的下一战场；其三，Rust clean-room 重写（wordcraft、cadcraft、nvidia-macos-driver）说明社区对「重写被垄断的基础软件」的兴趣在系统性上升。
来源与延伸阅读
接下来值得继续跟踪
- openai/math 的后续提交方向：是持续扩充语料，还是接入模型训练管线，将决定其是「数据集」还是「基础设施」。
- Skill 类项目（huashu-art-motion、replica-skill）能否沉淀出统一的 Skill 格式标准，观察是否出现跨平台兼容方案。
- wordcraft/cadcraft 的社区贡献活跃度：clean-room 重写项目常见高开低走，一个月后的 commit 频率是关键指标。
- nvidia-macos-driver 的硬件兼容列表与稳定性反馈，驱动项目的实际可用性需长期验证。
相关文章
OpenAI 开源数学库狂揽 1.3 万星
本周 GitHub 近 7 天新建热门仓库合计约 4.4 万 stars。最大亮点是 openai/math 以 13,083 星一骑绝尘；storytold 用纯 Rust 连发 Word、Excel、AutoCAD 三款 clean-room 重写项目；AI Agent 落地渗透测试、iPhone 控制与个人理财，安全与自动化成为主线。
2026-10-08OpenAI 开源数学仓库近万星领跑
本周 GitHub 新建热门仓库合计约 21,000+ stars。openai/math 以 9,527 星断层领先；最大趋势是「Agent Skill」类项目扎堆出现——answer-me-with-html、replica-skill、huashu-art-motion 都在教 Agent 干更具体的活。此外 Rust 工具链、本地大模型硬件协同、同人游戏复刻也各有亮点。