[1/3] 目前 HOL4 的定理库里缺少勒贝格积分和广义黎曼积分之间等价性的形式化证明，导致那些用初等数学函数构造的随机变量的数学期望无法用微积分基本定理和导数公式直接计算出来。我知道证明就在这本《A Modern Theory of Integration》里，我准备把它形式化出来，将来定理证明器没准儿可以变成一个初 ...全文