🔥 开源热榜

它把 BodyParts3D 的人体解剖数据变成能在浏览器里自由旋转的 3D 模型，2,234 个身体部位都可以单独点选，也能按系统分层查看、搜索或用爆炸视图拆开观察。过去要做这类交互解剖图需要专业医学数据或闭源商用授权，这个项目把数据和技术栈开放出来，主要解决“人体结构如何被快速、直观地理解”。你看到的不是静态图片，而是可交互的解剖模型；它既是医疗可视化底子，也是医学教育、科普产品可以直接用的原型。

它解决的是“品牌在 AI 回答里的可见度”这个新问题。现在很多人不再直接翻搜索页面，而是让 ChatGPT、Perplexity 等 AI 推荐品牌，是否被提及就取代了传统排名。这个项目把监测过程自动化：输入品牌与竞品，它会基于大模型或数据源生成可见度报告，对比谁更常出现在 AI 答案中，帮助判断竞品在生成式搜索里的心智份额。作为开源方案，它把原本要人工逐个 AI 对话测试再整理的工作，变成可重复运行的报告流程。

它让微信聊天记录变成一个可以通过命令行检索、能被 AI 代理调用的本地记忆。工作原因积攒在微信里的客户、合作消息太多时，这个系统会读取本地微信数据，以只读方式做搜索和结构化整理，每天生成简报、待跟进事项和潜在机会线索，还能作为 Codex 的技能来回答问题。相比把聊天记录导出到云端再由其他 AI 处理，它的卖点是“本地优先”：原始数据不出机器，AI 只使用检索到的局部上下文，兼顾隐私和可用性。

这是给 AI 创作工作流做的小型工作室：用一段文字描述或参考图，自动生成可编辑的 Blender 卡牌场景，同时做出一页可交互的 Three.js 展示页。关键不在于生成一张普通图片，而是生成真正能继续修改、能放进项目目录的 3D 资产，并保留用户要求的主题、风格、排版和用途。仓库以“skill”形式提供代码和运行逻辑，不预置生成好的素材；因此它更像是让 AI 助手学会完成一项完整设计任务，而不是一次性文生图 demo。

Claude Code、Cursor、Codex、Antigravity 这类 AI 编程工具都有订阅或用量限制，用户埋头写代码时常在关键时候才发现超限而停工。Codenotch 是 macOS 上的常驻小工具，把这些工具的用量数据集中起来，用一个小窗口钉在屏幕边缘，让你随时看到还剩多少。它解决的是多工具额度不可见的问题：不用每天打开几个后台页面计算余量，在编辑器旁边就能看到“还剩多少”。本质上像游戏 HUD，让稀缺资源始终处于视觉范围内。

从仓库名称和 Lean 语言判断，这是对费马大定理的一次形式化探索：用 Lean 定理证明器把数学命题、定义与推理过程写成可编译代码，让机器检查每一步是否逻辑自洽。人类读数学证明时可能接受“跳过细节”，Lean 不会。项目没有附加说明文字，因此不能确定它覆盖了完整的 Wiles 证明，还是聚焦在某个局部结论；但把这种大定理放进 Lean，本身就是在测试 AI 数学能力与证明库的边界。

这个项目试图打破 NVIDIA DLSS 5 神经网络渲染技术对自家显卡的绑定，让 AMD GPU 也能运行。DLSS 本身依赖深度模型与相关硬件调度，作者很可能是通过兼容层、驱动拦截或运行时替换让 A 卡接入，所以简介里用了“Magic”来形容。它解决的问题很直接：不想因为一项渲染技术换显卡，或者希望在 AMD 平台也获得类似效果。项目带有实验性质，兼容性、性能和画质都可能因驱动与游戏而异，需要自己调试验证。

这个仓库用 Lean 提供了一组“证书”，对应 Navier-Stokes 与 Euler 方程的研究结果。对流体力学这类分析性强的数学，不少结论需要精密的推导，人力检查容易出错；Lean 证书则把论证写成机器可验证的证明文件，让核心结果达到类似代码编译通过的强度。它不是给终端用户使用的软件，而是把论文或研究中的关键数学论断工程化：作者声称的定理或界，可以打开仓库逐条检查验证，减少“证明太长无法核对”带来的不确定性。