Direction 01
Isabelle/HOL 与可扩展的形式化证明结构
围绕子模贪心算法与近似保证，关心的不只是把一个定理证完，而是把证明、接口与后续扩展组织成能继续长大的 library。
Academic Landing
学术
入口页：方向、代表性材料、时间展开
我目前的学术工作主要围绕 OR for ML 展开，关心怎样把优化、形式化验证与结构化建模真正写成可检验、可复用、可继续推进的问题线。
这一部分围绕三层材料组织：当前研究方向、问题陈述与代表性工作。读者可以先从研究主线进入，再根据需要查看具体项目与阶段性笔记。
这里有些工作已经接近成熟的 formal development，有些仍是探索中的研究笔记。我保留这两类材料，是因为我关心的不只是最终结果，也包括一个问题如何逐渐变得可检验、可复用、可继续推进。
Academic Landing
Academic
A clear entry page: directions, evidence, then notes over time
My current academic work is organized through an OR-for-ML lens, with a recurring interest in making optimization, formal verification, and structured modeling explicit enough to be checked, reused, and extended.
This section is organized around three layers: current research directions, problem framing, and representative work. Readers can begin with the research lines and then move to project materials or technical notes as needed.
Some of these projects are mature formal developments; others are exploratory research notes. I keep both on the site because I care about showing not only final outputs, but also how a problem becomes structured enough to be checked.
Research Directions
三条目前较清楚地体现我问题意识的研究主线。
Research Directions
Three directions that currently offer the clearest view of how I frame problems.
Direction 02
不变性下的对偶、下界与结构恢复
当一个优化模型因平移不变性或对称性导致 natural dual collapse 时，我关注 collapse 之后仍可恢复的几何信息，尤其是它能否被组织成可解释的 structural score 或 lower-bound surrogate。
Direction 03
从连续对象到可检视结构的 prototype
围绕连续信号与事件流的离散化问题，我关注 prototype 如何保留结构、表达约束，并把直觉性的可操作要求转化为可检验的规则。
Direction 01
Isabelle/HOL and extendable proof structure
Through submodular greedy algorithms and approximation guarantees, I care not only about proving a theorem, but about organizing proofs, interfaces, and later extensions into a library that can keep growing.
Direction 02
Duality, lower bounds, and structure under invariances
When translation or symmetry causes the most natural dual constructions to collapse, I focus on the geometric information that survives, and whether it can be organized into an interpretable structural score or lower-bound surrogate.
Direction 03
Prototypes from continuous objects to inspectable structure
Around discretization problems for continuous signals and event streams, I am interested in how prototypes preserve structure, express constraints, and translate intuitive operational requirements into checkable rules.
Selected Highlights
三个进入当前 academic line 的具体入口对象。
Selected Highlights
Three concrete entry points into the current academic line.
Highlight 01
Isabelle/HOL：现代子模贪心算法形式化
目前最清楚地体现“把证明写成结构”的工作对象。
Highlight 02
当一个 dual 路线走不通时留下的结构
一条很新的线，正在把 collapse 之后真正留下的东西重新组织出来。
Highlight 03
Metalcore Piano Lab
把 prototype / discretization 这条线落到浏览器对象上的一个公开实验。
Highlight 01
Isabelle/HOL: modern submodular greedy formalization
The clearest current public example on the site of how I try to turn proofs into durable structure.
Highlight 02
What remains when a dual route fails
A newer line that is trying to reorganize what survives after the obvious dual constructions collapse.
Highlight 03
Metalcore Piano Lab
A public prototype that turns the prototype / discretization line into a concrete browser object.