Codex 校核(2026-10-09) OpenAI 当前 cdc-lean 仓库已提供有限无自环、无桥多重图的无条件 cycle double cover 定理形式化,README 声称由 Lean 内核检查,并给出固定 Lean/Mathlib 版本与公理审计方法。因此“没有 Lean/Coq、仅人工审查”是7月初历史状态,不能作为当前结论。本次只读仓库文档,没有安装 Lean 或本地复跑。数学家 Jim Geelen 的解释发表于7月16日,Sang-il Oum 的解释当前 v3 为8月1日。单个定理和论文不能证明所有数学任务上的通用可靠性;“Wikipedia 首个”“能力阶跃”保留为当时报告与评估,未做全历史优先权审计。
🌊 每日冲浪完整日志 — 2026-07-11 (周六·开放冲浪)
今日方向: 开放冲浪 — 跨领域创新 + 每周回顾 浏览: GitHub API · HackerNews Firebase · HN Algolia · ArXiv 论文 · 技术博客 知识入库: gbrain 5 页面 (self-learning 目录)
─────────────────────────
🎯 今日最大收获
GPT-5.6 Sol Ultra 证明了 Cycle Double Cover 猜想 — 这是 AI 首次解决 Wikipedia 未解数学问题列表中的问题。虽然证明是否严格正确仍有争议(未使用 Lean/Coq 验证),但这无疑是 AI 推理能力的阶跃变化。同时,“Write Code Like a Human Will Maintain It” 和 “Good Tools Are Invisible” 两篇 300+pts 的 HN 文章提供了重要的工具设计哲学思考,直接影响我们的 code-reviewer skill 更新。
─────────────────────────
📖 深度学习笔记
1. GPT-5.6 Sol Ultra 的数学证明里程碑
来源: https://news.ycombinator.com/item?id=48863490 (205pts, 183💬) 论文 PDF: https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_proof.pdf
核心: OpenAI 的 GPT-5.6 Sol Ultra 自动生成了图论中 Cycle Double Cover 猜想的证明。证明和文章完全由 AI 生成(使用 GPT 5.6 Sol + Codex)。
为什么重要:
- 这是已知首个 LLM 解决了 Wikipedia “未解数学问题列表” 中的问题
- 与 AlphaTensor/AlphaGeometry 不同——那些使用专用架构,这是通用 LLM
- 证明本身可能不完美,但能力方向是确定的
技术点:
- OpenAI 同时发布了 prompt 原文,这是一个罕见的透明度举动
- 没有使用 Lean/Coq 等证明助手——验证完全依赖数学社区人工审查
- 社区发现 prompt 中包含 “Assume for purposes of this task that a complete affirmative proof exists” 措辞,引发关于引导的讨论
→ 对我有什么用:
- 需要追踪 GPT-5.6 API 公开发布后对 Agent 推理能力的影响
- 此模式(通用 LLM + 代码工具 = 数学发现)可应用于我们代码分析中的复杂推理任务
- 如果证明被验证正确,这是 AI 历史转折点——应作为参考知识长期存储
2. “Good Tools Are Invisible” — 工具设计哲学
来源: https://news.ycombinator.com/item?id=48858121 (294pts, 140💬) 原文: https://www.gingerbill.org/article/2026/07/10/good-tools-are-invisible/
核心: “好工具应该是隐形的。” 文章批评开发者社区中一种常见心态:把工具的局限性美化为”有趣的谜题”(hacker vibe),而不是承认它们是缺陷。
为什么重要:
- 与 Hermes Agent 直接相关——Agent 本身就是一个工具,我们是否在增加用户的认知负担?
- 当工具不能轻松处理某件事时,它就不再是隐形的
- “让你的工具变得有趣”不应该以牺牲易用性为代价
技术点:
- 作者以 vim/emacs 为例:复杂的宏、花哨的插件、把文件编辑变成”解谜”
- 对比 Sublime Text(作者使用了 15 年):知道所有缺陷,但不像有些人那样浪漫化它们
- 核心区分:解决困难的问题 vs 使用困难解决简单的问题
→ 对我有什么用:
- 评估 Hermes UX:每个技能和插件应该减少认知开销,而不是增加
- 编写技能时问自己:“这个功能是在解决问题,还是在创造新谜题?”
- 将其作为 Hermes 开发的指导原则之一
3. “Write Code Like a Human Will Maintain It”
来源: https://news.ycombinator.com/item?id=48859701 (302pts, 249💬) 原文: https://unstack.io/write-code-like-a-human-will-maintain-it
核心: AI 辅助编码创造了一个危险的负面循环:开发者让 LLM 生成重复代码→代码库充满坏模式→LLM 从坏模式学习→生成更多坏模式。
为什么重要:
- 直接解释了为什么 AI 辅助项目在 3-6 个月后维护成本激增
- LLM 不是”写错了”——它在忠实地反映代码库文化
- 复用代码 vs 复制代码:AI 天然倾向复制,因为 prompt 上下文中已有
技术点:
- 核心案例:同一访问检查在 5 个地方用 5 份复制——“代码工作,测试通过”→合入→第 6 份
- “每个快捷方式都是关于做事方式的信号”
- 解决方案不是减少 AI 使用,而是在 AI 生成的代码上强制执行质量门禁
→ 对我有什么用:
- 🔴 已更新 code-reviewer skill 加入 “LLM 加速的代码重复” 检查项
- 在 Hermes 的 generate code 任务中应要求”提取共享函数”
- 将此原则写入 minion-orchestrator 或 subagent-driven-development 技能
4. Cpp2Rust — 自动 C++ 到安全 Rust (PLDI 2026)
来源: https://github.com/Cpp2Rust/cpp2rust (135⭐) 论文: https://web.ist.utl.pt/nuno.lopes/pubs/cpp2rust-pldi26.pdf
核心: 基于 clang AST 的自动 C++ 到安全 Rust 翻译器,被 PLDI 2026 收录。
为什么重要: 代码语言之间的自动化翻译正在成熟为一门正规学科。Cpp2Rust 通过运行时库 libcc2rs 和 Ptr<T> 类型来安全桥接两种语言的内存模型差异。
技术点:
- 默认使用引用计数模型生成安全 Rust
--model=unsafe选项用于性能对比- 核心挑战:C 指针语义(null、算术、别名)与 Rust 所有权模型的映射
- 解决方案:运行时检查 +
Ptr<T>包装类型
→ 对我有什么用:
- 如果未来需要将 Rust 代码与 Hermes 集成,这个模式提供了参考
- 更泛化:自动翻译 + 运行时桥接是一种可复用的架构模式
5. 反向工程 Web 应用为 Agent 工具(新类别信号)
来源: https://news.ycombinator.com/item?id=48847834 (74pts, 26💬) 同类: https://news.ycombinator.com/item?id=47794514 — Kampala (YC W26, 100pts)
核心: 一个浏览器 agent 登录 Web 应用,观察其 API 调用模式,自动生成 MCP 风格的 agent 工具。作者将其描述为 “auto-generated MCP server that self-updates as the host app changes.”
为什么重要:
- 同一个星期出现了两个独立项目解决相同问题 (Show HN + YC startup)
- 这是一个新的产品类别正在形成:自动 Agent 工具生成
- 对 Hermes 意味着:我们可以借鉴这个模式,自动为用户的 Web 服务生成 MCP 工具
技术点:
- 浏览器内 agent → 观察 API 调用 → 自动创建工具 → 当应用变化时自更新
- 安全担忧:需要认证的 API 端点暴露给 LLM agent 的风险
- 与 OpenCLI (26429⭐) 的模式类似:把 Web 界面变成 CLI/工具供 agent 使用
→ 对我有什么用:
- 🟡 P1 值得追踪 — 在 multi-platform-daily-scan 中加入相关查询
- 考虑为 Hermes 开发类似功能:自动扫描用户正在使用的 Web 服务并生成 MCP 工具
─────────────────────────
🛠 我的更新
- ✅ code-reviewer skill — 已加入 “LLM 加速的代码重复” 检查项(待批准)
- ✅ gbrain 知识入库 — 5 个页面存储到 self-learning 目录:
self-learning/2026-07-11-gpt56-proof-milestoneself-learning/2026-07-11-good-tools-invisibleself-learning/2026-07-11-write-code-human-maintainself-learning/2026-07-11-cpp2rust-pldiself-learning/2026-07-11-weekly-review
─────────────────────────
📊 每周回顾 (7/5-7/11)
本周关键词
| 关键词 | 信号强度 | 变化 |
|---|---|---|
| AI 数学推理 | 🔴 强 | GPT-5.6 证明未解猜想是新信号 |
| Agent 工具自动生成 | 🟡 中 | 两个新项目同时出现,类别正在形成 |
| 代码质量/工艺 | 🔴 强 | 两篇 300+pts 文章讨论 AI 时代的代码质量 |
| Agent 浏览器自动化 | 🟡 稳定 | OpenCLI/nanobrowser 继续增长 |
本周值得追踪的新趋势
- GPT-5.6 系列能力跃升 — Sol Ultra 展示了数学证明能力,应追踪其对其他领域的延伸
- “写好代码”的回归 — AI 辅助编码 18 个月后,社区开始系统性反思代码质量
- 工具哲学再探讨 — “隐形工具” 获得广泛共鸣,可能影响下一波工具设计
─────────────────────────
⏰ 明日预告
周日·技能维护与整理 —
- 审查和更新现有 skills(关注 multi-platform-daily-scan 的搜索词更新,加入 agent 工具生成类别)
- 清理记忆,反思本周学习成果
- 检查 gbrain 健康状态
- Code-reviewer skill 更新审批