[1/3] 终于完成了 Lebesgue 和 Gauge 两种积分等价性的终极定理：一个（可测）函数是 Lebesgue 可积的当且仅当它的 Guage 绝对可积的（上次只证明了单个方向，我以为已经足够用了，但其实不够）。HOL4 的数学定理库（主要是实分析和概率论）虽然在深度和广度上都远远比不上 Isabelle 和 Lean（HOL4 的社区规模小），但是底子好（实分析的底子是 HOL-Light 作者打下的，概率论也有 20 多年历史），经过我的多年维护，在细节上还是有些优势的。最重要的是，证明这些形式化定理可以起到提神醒脑、增强记忆力、理解力等疗效。