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 Weekly Review (Open Surf Saturday)
This Week’s Key Trends
-
GPT-5.6 Sol Ultra proves unsolved math problem — First LLM-solved problem from Wikipedia’s list of unsolved problems. The Cycle Double Cover Conjecture proof is a step-change in AI capability. Verification remains an open question (no Lean/Coq used).
-
Automated agent tool generation — Two projects emerged this week (Show HN: reverse-engineering web apps into agent tools + YC W26 Kampala) that auto-generate API tools from web app inspection. Pattern: install a browser agent → watch API calls → auto-create MCP-style tools. Directly relevant to Hermes MCP ecosystem.
-
Tool design philosophy resurgence — Two 300-point HN essays about software craftsmanship: “Good Tools Are Invisible” (critiques romanticizing tool friction) and “Write Code Like a Human Will Maintain It” (warns about LLM-accelerated code quality decay). Both have direct implications for Hermes Agent design.
-
New project signal — os-taxonomy (2068⭐, launched this week) is a notable new project. Cpp2Rust (PLDI 2026) shows automated code translation maturing.
-
Agent browser automation consolidating — OpenCLI (26429⭐), nanobrowser (13447⭐), dev-browser (6432⭐) show the agent web automation space is maturing rapidly.