01
形式结构
Isabelle/HOL 下对子模 greedy 算法的形式化。
Selected Evidence
01
Isabelle/HOL 下对子模 greedy 算法的形式化。
02
对偶、invariance,以及 collapse 之后的 structural scoring。
03
前卫摇滚 / metalcore 写作、贝斯与吉他的编排,以及自制曲目。
04
把摄影当作关于光线、距离、天气与记忆的练习。
已完成总量九千六百多行的 thy 文件,正在准备 clean up 发 AFP。
更新了一波新音源和插件,正在尝试把以前的歌大部分替换新混音。
发现所有拉格朗日对偶都会崩塌到 trivial 的 0 bound,只有 conjugate 对偶有 nontrivial 的可能性,所以正在往这个方向继续探索,看看能不能把对偶做成某种打分器。
当两条最自然的 Lagrangian dual 路线都塌到 trivial 0 bound 之后,留下来的反而是一个和 Range(B)、cycle consistency 与 instance difficulty 相关的 dual-based structural score。
Read More从 classical greedy 的 theorem line,走到 LazyGreedy extension、StochasticGreedy skeleton 与一套可继续扩展的 Isabelle/HOL library。
Read More从连续音频到可玩的谱面:起音检测、节拍网格、段落对齐与可玩性约束。
Read More从纯数学走向优化研究:一个学期的研究训练与新的问题切入口。
Read More查看完整的数学栏目文章列表与更新记录。