Isabelle/HOL：现代子模贪心算法形式化

问题： 在 Isabelle/HOL 中形式化验证基数约束下单调非负子模最大化的近似算法理论，覆盖 classical greedy、LazyGreedy 与 StochasticGreedy，并组织其近似保证、算法构造与 oracle-cost 分析。

方法： 采用基于 locale 的模块化组织方式，将抽象假设、算法构造、step-spec / recurrence 证明、具体实例解释以及复杂度 / oracle-cost 层分开处理，以保持证明结构清晰且便于后续扩展。

目前阶段： 经典 greedy 基线已完成；LazyGreedy 已形成完整的 stateful、approximation 与 oracle-cost 结构；StochasticGreedy 已完成 concrete uniform with-replacement theorem line，并达到最终近似定理包装这一关键里程碑。

下一步： 继续进行整理与打磨，包括 stochastic 部分的命名与注释统一、依赖清理、成本比较叙事加强，以及面向 AFP / submission-style 的 presentation refinement。

当前状态： 进行中（核心定理线已完成，正在整理与提升展示质量）。

不变性下的对偶与下界

问题： 对于某些由图上的相对差分定义出的距离拟合目标，自然写出的对偶形式会因为平移不变性或相关的不可识别性而退化，最终只能给出无信息的下界。

方法： 比较 Fenchel/DC 与 Lagrangian 两条路线，并逐步检查：是哪个不变性让消元后的下界变成平凡结果，以及加入什么约束后情况会改变。

目前阶段： 我已经把几条主要推导路线重新走通，也比较清楚地看到平凡下界是在哪一步出现的。

下一步： 继续测试 gauge-fixing、增广或更紧约束是否足以恢复非平凡下界。

当前状态： 进行中。

Metalcore Piano Lab｜从音频 / MIDI 到谱面（WIP）

这个原型在做的事情很直接：把连续的音频或 MIDI 输入，变成可玩的节奏游戏谱面事件。技术上它牵涉起音检测、拍点跟踪、分段、对齐，以及一组并不完全稳定的可玩性约束。

我已经做了一个浏览器版本，用来反复测试这些假设在实际输入上会怎样失效。现在更关心的，是谱面质量该怎么评估，以及哪些约束只是方便实现，哪些是真的必要。

当前状态： 开发中。

Isabelle/HOL: Formalizing Modern Submodular Greedy Algorithms

Problem: Formalize in Isabelle/HOL the approximation theory for monotone nonnegative submodular maximization under a cardinality constraint, covering classical greedy, LazyGreedy, and StochasticGreedy, together with their approximation guarantees, algorithmic constructions, and oracle-cost analyses.

Methods: A locale-based modular organization that separates abstract assumptions, algorithmic constructions, step-spec / recurrence proofs, concrete instance interpretations, and complexity / oracle-cost layers, so that the proof structure remains clear and extensible.

Current stage: The classical greedy baseline is complete; LazyGreedy now has a full stateful, approximation, and oracle-cost development; StochasticGreedy has completed a concrete uniform with-replacement theorem line and reached the key milestone of packaging the final approximation theorem.

Next step: Continue the clean-up and refinement: unifying names and comments in the stochastic part, pruning dependencies, strengthening the cost-comparison narrative, and improving the presentation toward an AFP / submission-style version.

Current status: Ongoing (the core theorem lines are complete; current work is focused on clean-up and presentation quality).

Duality and Lower Bounds under Invariances

Problem: For certain distance-fitting objectives defined through graph-relative differences, natural dual formulations may collapse because of translation invariance or related non-identifiability.

Methods: Comparison of Fenchel/DC and Lagrangian routes, followed by structural analysis of where the degeneration comes from and what extra constraints or modifications may be needed.

Current stage: I have worked through the main derivations and clarified where the trivial lower bound appears.

Next step: Test whether gauge-fixing, augmentation, or tighter constraints are enough to recover a nontrivial bound.

Current status: Ongoing.

Metalcore Piano Lab | Audio / MIDI to Chart (WIP)

This prototype is doing something fairly concrete: taking continuous audio or MIDI input and turning it into playable rhythm-game chart events. In practice that means onset detection, beat tracking, segmentation, alignment, and a set of playability constraints that are not yet fully settled.

I have built a browser version mainly as a way to test where those assumptions break on real inputs. What interests me most at the moment is how chart quality should be evaluated, and which constraints are genuinely necessary rather than just convenient for implementation.

Current status: Work in progress.