按时间归档研究记录，也保留一层问题线索标签，方便从 Isabelle/HOL、Duality、OR for ML 与 Prototype 这几条线扫过去。
2026-05-22
三月留下来的 dual score 原本只是 instance-level structural score；最近它开始和 differentiable stationary points、stationary dual witness、projected retention、Hessian negative curvature 以及 cycle-rank saddle certificates 接起来。
阅读全文2026-05-22
在等待前一个 AFP 项目流程继续推进期间，我开始整理第二个 Isabelle/HOL optimization 项目：从 smooth convexity、projection geometry、descent estimates 到 projected-gradient mapping 和 residual certificates，尝试把 projected-gradient descent 写成一套可复用的 first-order methods infrastructure。
阅读全文2026-03-23
当两条最自然的 Lagrangian dual 路线都塌到 trivial 0 bound 之后，留下来的反而是一个和 Range(B)、cycle consistency 与 instance difficulty 相关的 dual-based structural score。
阅读全文2026-03-14
从 classical greedy 的 theorem line，走到 LazyGreedy extension、StochasticGreedy skeleton 与一套可继续扩展的 Isabelle/HOL library。
阅读全文2026-02-07
从连续音频到可玩的谱面：起音检测、节拍网格、段落对齐与可玩性约束。
阅读全文2026-01-29
从纯数学走向优化研究：一个学期的研究训练与新的问题切入口。
阅读全文2025-12-29
在 Isabelle 中形式化单调子模函数下贪心算法的近似保证。
阅读全文2025-10-18
把可验证性嵌进证明过程：从动机到 Nemhauser–Wolsey theorem。
阅读全文