Isabelle/HOL：现代子模贪心算法形式化
题目： 面向基数约束下单调非负子模最大化的 Isabelle/HOL 形式化，覆盖 classical greedy、LazyGreedy 与 StochasticGreedy，并包含近似保证与 oracle-cost 结构。
当前状态： 核心定理线已完成；目前在做 clean-up、依赖整理与 AFP 风格打磨
选定项目
这里是项目材料与公开产出的索引。每个条目只保留题目、当前状态，以及可以直接查看的材料。
Selected Projects
This page is an index of project materials and public outputs. Each entry keeps only the topic, current status, and the materials that can be viewed directly.
研究与形式化验证
Research and Formal Verification
不变性下的对偶与下界
题目： 带图相对结构的距离拟合目标里，对偶与下界为何会在平移不变性或不可识别性下退化。
当前状态： 进行中
Isabelle/HOL: Formalizing Modern Submodular Greedy Algorithms
Topic: An Isabelle/HOL formalization for monotone nonnegative submodular maximization under cardinality constraints, covering classical greedy, LazyGreedy, and StochasticGreedy, together with approximation and oracle-cost structure.
Current status: Core theorem lines complete; current work focuses on clean-up, dependency refinement, and AFP-style presentation
Duality and Lower Bounds under Invariances
Topic: Notes and ongoing derivations on why natural duals collapse for certain translation-invariant distance-fitting objectives, and what structural modifications may change that.
Current status: Ongoing
原型与信号处理
Prototype and Signal Processing
工程与 IP
Engineering and IP
防离析布料系统
题目： 一个面向真实布料场景、用于降低砂石离析的工程系统。
当前状态： 在审 / 已授权
Anti-Segregation Spreading System
Topic: An engineering system designed to reduce aggregate segregation during spreading operations.
Current status: Pending / Granted
数据分析
Data and Analytics
Funnel / Retention / Attribution Analysis
题目： 应用数据分析中的转化、留存与归因诊断。
当前状态： 已完成
Funnel / Retention / Attribution Analysis
Topic: Conversion, retention, and attribution diagnostics in applied data analysis.
Current status: Completed