2026-03-23 · 约 5 分钟
当一个 dual 路线走不通时，我真正得到的东西
当两条最自然的 Lagrangian dual 路线都塌到 trivial 0 bound 之后，留下来的反而是一个和 Range(B)、cycle consistency 与 instance difficulty 相关的 dual-based structural score。
阅读全文数学文章
研究记录、实验笔记与结构化的思考。
from medium.com/@syedalihamza23/fun-with-fractals-julia-2a007e587650
2026-03-14 · 约 6 分钟
从一个定理到一套框架：我的 Isabelle 子模优化项目新进展
从 classical greedy 的 theorem line，走到 LazyGreedy extension、StochasticGreedy skeleton 与一套可继续扩展的 Isabelle/HOL library。
阅读全文2026-02-07 · 约 3 分钟
Metalcore Piano Lab｜从音频到谱面：一个离散化的实验（WIP）
从连续音频到可玩的谱面：起音检测、节拍网格、段落对齐与可玩性约束。
阅读全文2026-01-29 · 约 2 分钟
Spring 2026｜新科研记录的开始
从纯数学走向优化研究：一个学期的研究训练与新的问题切入口。
阅读全文2025-12-29 · 约 4 分钟
一个正在进行的 Isabelle 研究项目：Submodular Greedy 的形式化
在 Isabelle 中形式化单调子模函数下贪心算法的近似保证。
阅读全文2025-10-18 · 约 2 分钟
我的第一个 Isabelle 形式化证明
把可验证性嵌进证明过程：从动机到 Nemhauser–Wolsey theorem。
阅读全文