[4/3] 概率论中心极限定理（李雅普诺夫的版本）的形式化证明基本完成了。我这边已经没什么可写的了，还剩最后一个比较麻烦的积分运算（正态分布的四次方）外包给我的越南学生了（毕竟她是论文的第一作者）。我就等她先向 HOL4 提交 PR 然后我就可以提交我的代码了（过去一周时间写了四千多行）。同时我可以开始着手写论文框架和部分章节的草稿了。要是能在（5月）论文投稿前找到个学校挂名就更好了，刚入职即发表一篇论文。
发布于 辽宁