田春冰河的技术动态
田春冰河
2020-02-04 00:00:00 发布
[3/3] 我今天形式化证明了一个勒贝格积分里相当基础的结果：每个 Borel 可测函数在零测度集上都是可积的，进而其积分为零。看似简单的结论，但证明过程相当复杂，因为零测度集可能很大，甚至是不可数的，而这个函数本身可能在相当多的点上取值正无穷或负无穷，证明几乎用到了所有更底层的基础定理。
2020-02-04 00:00:00 发布
[3/3] 我今天形式化证明了一个勒贝格积分里相当基础的结果：每个 Borel 可测函数在零测度集上都是可积的，进而其积分为零。看似简单的结论，但证明过程相当复杂，因为零测度集可能很大，甚至是不可数的，而这个函数本身可能在相当多的点上取值正无穷或负无穷，证明几乎用到了所有更底层的基础定理。
田春冰河
2020-02-01 00:00:00 发布
[2/3] 我从圣诞节期间就开始日夜奋战形式化数学定理，到今天终于完成了 HOL 测度和概率论的第二阶段工作，包括之前所有困扰我的问题都解决了，又给官方提交了一个 5000 多行代码的巨大 PR，接下来几天可以总结成果写篇论文了。目前我在所有贡献者里按新增代码行数排名第七。
网页链接
2020-02-01 00:00:00 发布
[2/3] 我从圣诞节期间就开始日夜奋战形式化数学定理，到今天终于完成了 HOL 测度和概率论的第二阶段工作，包括之前所有困扰我的问题都解决了，又给官方提交了一个 5000 多行代码的巨大 PR，接下来几天可以总结成果写篇论文了。目前我在所有贡献者里按新增代码行数排名第七。
网页链接
田春冰河
2020-01-15 17:03:38 发布
[1/3] 我干了好几年的概率论（测度论）形式化工作的首篇论文还差最后一个定理（实数集上勒贝格测度的存在和唯一性）就可以开始写了，但就卡在这个定理上。这个证明的第一部分很巧妙，需要用到有限开覆盖定理，所以书上详细介绍；第二部分 “it is not hard to see...” 是不难，但深究起来极其麻烦。
2020-01-15 17:03:38 发布
[1/3] 我干了好几年的概率论（测度论）形式化工作的首篇论文还差最后一个定理（实数集上勒贝格测度的存在和唯一性）就可以开始写了，但就卡在这个定理上。这个证明的第一部分很巧妙，需要用到有限开覆盖定理，所以书上详细介绍；第二部分 “it is not hard to see...” 是不难，但深究起来极其麻烦。
田春冰河
2020-01-10 19:08:52 发布
[1/3] 话说前天我提交给 HOL 官方的 400 多行代码——就是我跟大小老板合写的论文里某定理的形式化版本——已经顺利被合并了。这样我在 HOL 贡献者排名里按照新增代码行数还差不到一千行就可以晋级了。结果没想到给 HOL 提交 PR 比正式发表论文还管用，排名第二的 Konrad Slind，一个比我早学定理证明 ...全文
2020-01-10 19:08:52 发布
[1/3] 话说前天我提交给 HOL 官方的 400 多行代码——就是我跟大小老板合写的论文里某定理的形式化版本——已经顺利被合并了。这样我在 HOL 贡献者排名里按照新增代码行数还差不到一千行就可以晋级了。结果没想到给 HOL 提交 PR 比正式发表论文还管用，排名第二的 Konrad Slind，一个比我早学定理证明 ...全文
田春冰河
2019-12-09 22:07:36 发布
[2/3] 在 Runtime Verification 领域有很少几篇论文是基于规则引擎的，就是研究怎么能用 Rete 算法来高效简洁地实现整个过程。巧了，我也是这方面的爱好者，而且手里有价值五千刀的规则引擎（KnowledgeWork）一直苦恼无法收回投资呢。上周初步尝试了一下，基本上是可行的。我准备写一篇更好的论文。
2019-12-09 22:07:36 发布
[2/3] 在 Runtime Verification 领域有很少几篇论文是基于规则引擎的，就是研究怎么能用 Rete 算法来高效简洁地实现整个过程。巧了，我也是这方面的爱好者，而且手里有价值五千刀的规则引擎（KnowledgeWork）一直苦恼无法收回投资呢。上周初步尝试了一下，基本上是可行的。我准备写一篇更好的论文。
田春冰河
2019-12-06 18:07:55 发布
[1/3] 我有一个问题百思不得其解：当我在 VS 里创建新工程的时候，哪怕是完全不使用 .NET 的工程，它也让我选某个版本 .NET 框架。问题是如果我当初选的那个版本，比如 4.0，在另一台电脑里根本没有安装的话，那我这个工程在那台机器的上就无法编译了，工程属性里也找不到修改 .NET 依赖版本的地方。
2019-12-06 18:07:55 发布
[1/3] 我有一个问题百思不得其解：当我在 VS 里创建新工程的时候，哪怕是完全不使用 .NET 的工程，它也让我选某个版本 .NET 框架。问题是如果我当初选的那个版本，比如 4.0，在另一台电脑里根本没有安装的话，那我这个工程在那台机器的上就无法编译了，工程属性里也找不到修改 .NET 依赖版本的地方。
田春冰河
2019-11-21 20:49:55 发布
[1/3] 今天上午遇到一个 PDF，书签里全是大写字母，本质上是因为 AMS LaTeX 模板会将论文标题全部大写字母化。于是我给自己的 Acrobat 插件里添加了一个新功能：一键转换所有书签标题，每个单词首字母大写。代码是恶心的，但效果是正确的，把英语介冠词，特定缩写和罗马数字都考虑进去了。
2019-11-21 20:49:55 发布
[1/3] 今天上午遇到一个 PDF，书签里全是大写字母，本质上是因为 AMS LaTeX 模板会将论文标题全部大写字母化。于是我给自己的 Acrobat 插件里添加了一个新功能：一键转换所有书签标题，每个单词首字母大写。代码是恶心的，但效果是正确的，把英语介冠词，特定缩写和罗马数字都考虑进去了。
田春冰河
2019-11-14 18:06:39 发布
[1/3] 终于忙里偷闲把《猎魔人》原著小说7本都看完了，很爽，很多剧情在游戏里也遇到过。但还是看得不过瘾，因为故事并没有彻底讲完。我在网上好不容易才找到的，纯文本格式，然后我自己转成 PDF 再把原始文本变成附件以供日后重新排版。想看的可以从我这里下载：网页链接
2019-11-14 18:06:39 发布
[1/3] 终于忙里偷闲把《猎魔人》原著小说7本都看完了，很爽，很多剧情在游戏里也遇到过。但还是看得不过瘾，因为故事并没有彻底讲完。我在网上好不容易才找到的，纯文本格式，然后我自己转成 PDF 再把原始文本变成附件以供日后重新排版。想看的可以从我这里下载：
网页链接
田春冰河
2019-10-30 00:00:00 发布
[1/3] 最近我一边看《巫师》原著小说，一边在 Switch 上重玩《巫师3》的新手村部分，双倍的快乐。自从我在 PC 上安装了《巫师3》HD 重制 mod 以后，两个平台上的画质差距已经是天壤之别了，但 Switch 是接 TV 玩的，画质虽差（反正我近视眼）但十分流畅，Switch Pro 手柄也很好用，所以其实还不错。
2019-10-30 00:00:00 发布
[1/3] 最近我一边看《巫师》原著小说，一边在 Switch 上重玩《巫师3》的新手村部分，双倍的快乐。自从我在 PC 上安装了《巫师3》HD 重制 mod 以后，两个平台上的画质差距已经是天壤之别了，但 Switch 是接 TV 玩的，画质虽差（反正我近视眼）但十分流畅，Switch Pro 手柄也很好用，所以其实还不错。
田春冰河
2019-10-28 00:00:00 发布
[1/3] 几经周折，终于把 Henstock–Kurzweil 积分合并到 HOL4 里了，22614 行新代码。我现在在 HOL 贡献者里按新增代码行数排名，很快就要排到第 6 了，按提交数排名由于其他 PR 的缘故也进步喜人。
2019-10-28 00:00:00 发布
[1/3] 几经周折，终于把 Henstock–Kurzweil 积分合并到 HOL4 里了，22614 行新代码。我现在在 HOL 贡献者里按新增代码行数排名，很快就要排到第 6 了，按提交数排名由于其他 PR 的缘故也进步喜人。
田春冰河
2019-10-23 00:00:00 发布
[1/3] 我给 HOL4 贡献的概率论代码是以 Concordia HVG 那帮人的工作为基础的，因为我从他们官网下载的证明代码根本无法编译，所以我一直在做的就是修复他们的代码然后提交给 HOL 官方。昨天我去拉他们的最新代码时发现他们竟然反过来也抄我的代码，还管我叫 "HOL4 github developer"。我表示开心。
2019-10-23 00:00:00 发布
[1/3] 我给 HOL4 贡献的概率论代码是以 Concordia HVG 那帮人的工作为基础的，因为我从他们官网下载的证明代码根本无法编译，所以我一直在做的就是修复他们的代码然后提交给 HOL 官方。昨天我去拉他们的最新代码时发现他们竟然反过来也抄我的代码，还管我叫 "HOL4 github developer"。我表示开心。
田春冰河
2019-10-10 01:29:42 发布
[1/3] 原来 Springer 出版的会议论文集在会议召开期间会临时开放下载权限，让所有与会者都能下载到整本论文集的 PDF。虽然表面上看论文集仍然是卖钱的，但如果通过 DOI 或者 Springer Link 访问的话就可以公开下载了。我要趁机把整个 FM 2019 和所有子会议的论文集全部搞到。网页链接
2019-10-10 01:29:42 发布
[1/3] 原来 Springer 出版的会议论文集在会议召开期间会临时开放下载权限，让所有与会者都能下载到整本论文集的 PDF。虽然表面上看论文集仍然是卖钱的，但如果通过 DOI 或者 Springer Link 访问的话就可以公开下载了。我要趁机把整个 FM 2019 和所有子会议的论文集全部搞到。
网页链接
田春冰河
2019-09-27 21:58:17 发布
[1/3] 有些人啊，给开源项目提交了 PR 以后被凉在那里几天就着急了，一个劲儿地问怎么回事。你看我就不着急，因为咱的声誉良好，迟早会 merge 的。再说几万行的代码总要给维护者和其他人几天时间想一想，我自己也趁机歇息一下。而且我还理解维护者自己也需要时间写一些代码，不能光 merge 别人的。
2019-09-27 21:58:17 发布
[1/3] 有些人啊，给开源项目提交了 PR 以后被凉在那里几天就着急了，一个劲儿地问怎么回事。你看我就不着急，因为咱的声誉良好，迟早会 merge 的。再说几万行的代码总要给维护者和其他人几天时间想一想，我自己也趁机歇息一下。而且我还理解维护者自己也需要时间写一些代码，不能光 merge 别人的。
田春冰河
2019-09-26 22:57:58 发布
[2/3] 我们组官网上列出的整个组最近十篇论文，其中三篇我是一作和事实一作，距离我去年那篇会议论文都已经一年过去了。由此可见整个组里二三十人一年总共也发不了几篇论文。这次我可能也是 FBK 唯一去参加 FM 2019 会议的。过些日子等我的期刊论文发出来以后吓死他们 网页链接
2019-09-26 22:57:58 发布
[2/3] 我们组官网上列出的整个组最近十篇论文，其中三篇我是一作和事实一作，距离我去年那篇会议论文都已经一年过去了。由此可见整个组里二三十人一年总共也发不了几篇论文。这次我可能也是 FBK 唯一去参加 FM 2019 会议的。过些日子等我的期刊论文发出来以后吓死他们 网页链接
田春冰河
2019-09-26 19:57:58 发布
[1/3] 过去三天里我一鼓作气把 HOL Light 的形式化微积分给移植到 HOL4 里了。之前 HVG Concordia 的人打下了良好基础，但总共 700 多个定理中还有 30 多个无法完成，我从简单的开始逐个击破，只花了两天就全搞定了。我又给 HOL 提交了两万行代码，还在官方手册新增了一章 “高等数学”，等待审核。
2019-09-26 19:57:58 发布
[1/3] 过去三天里我一鼓作气把 HOL Light 的形式化微积分给移植到 HOL4 里了。之前 HVG Concordia 的人打下了良好基础，但总共 700 多个定理中还有 30 多个无法完成，我从简单的开始逐个击破，只花了两天就全搞定了。我又给 HOL 提交了两万行代码，还在官方手册新增了一章 “高等数学”，等待审核。
田春冰河
2019-09-23 21:42:22 发布
[2/3] 原来大学时学的微积分理论有很大一部分已经过时了，黎曼积分已经被形式更优美的 Henstock–Kurzweil 积分（也称为 gauge integral）取代了，这也是目前几大定理证明器里自带的形式化微积分。当初几个发明人还联合发出公开信要求教科书作者抛弃黎曼积分，但好像没人鸟他们。我决定好好学一下。
2019-09-23 21:42:22 发布
[2/3] 原来大学时学的微积分理论有很大一部分已经过时了，黎曼积分已经被形式更优美的 Henstock–Kurzweil 积分（也称为 gauge integral）取代了，这也是目前几大定理证明器里自带的形式化微积分。当初几个发明人还联合发出公开信要求教科书作者抛弃黎曼积分，但好像没人鸟他们。我决定好好学一下。
田春冰河
2019-09-23 21:42:22 发布
[1/3] OCaml 真是一个充满恶意的编程平台，几乎每一个用这种语言写的软件都严重依赖于特定版本的特定编译选项，外层还有一个独立的 Camlp5 来改进语法。最可恨的是，作为一个交互环境不支持导出内存映像。我为了运行 hol-light，不得不学会使用 OPAM，然后把自己固定在特定的旧版本组合上。
2019-09-23 21:42:22 发布
[1/3] OCaml 真是一个充满恶意的编程平台，几乎每一个用这种语言写的软件都严重依赖于特定版本的特定编译选项，外层还有一个独立的 Camlp5 来改进语法。最可恨的是，作为一个交互环境不支持导出内存映像。我为了运行 hol-light，不得不学会使用 OPAM，然后把自己固定在特定的旧版本组合上。
田春冰河
2019-09-20 00:00:00 发布
[1/3] 我自从去年7月份以来耗费无数心血的 HOL 概率论形式化工作，终于提交了首批代码。新增2万6千多行，删除1万7千多行，改动了 101 个文件，连 PR 的描述长度可能都是本项目前所未有。结果没过几个小时就被合并了，这是多大的鼓励和信任！我现在按删除代码行数已经前进了一个名次，排名第6了
2019-09-20 00:00:00 发布
[1/3] 我自从去年7月份以来耗费无数心血的 HOL 概率论形式化工作，终于提交了首批代码。新增2万6千多行，删除1万7千多行，改动了 101 个文件，连 PR 的描述长度可能都是本项目前所未有。结果没过几个小时就被合并了，这是多大的鼓励和信任！我现在按删除代码行数已经前进了一个名次，排名第6了
田春冰河
2019-09-17 00:00:00 发布
[1/3] 没想到我刚刚完成 CCS 论文回到概率论形式化的课题上就取得小进展了。之前 HOL 里由于合并来自 HOL-Light 的代码导致有两个互相冲突的实数集下确界定义，必须把其中一个删除或转化成等价定理才能确保所有相关定理同时使用。这个问题我 2 月份的时候没能解决，但从 HOL 维护者那里得到了提示。
2019-09-17 00:00:00 发布
[1/3] 没想到我刚刚完成 CCS 论文回到概率论形式化的课题上就取得小进展了。之前 HOL 里由于合并来自 HOL-Light 的代码导致有两个互相冲突的实数集下确界定义，必须把其中一个删除或转化成等价定理才能确保所有相关定理同时使用。这个问题我 2 月份的时候没能解决，但从 HOL 维护者那里得到了提示。
田春冰河
2019-09-11 00:00:00 发布
[3/3] 我这篇论文写得太好了，太重要了，目测将颠覆该理论诸多专家的认知。我用一页半纸才严格证明的一个结论当年在 Milner 的论文里竟然只有一行，这里面水有多深他当时肯定没看出来。我现在就等 Sangiorgi 三天内看了这个证明以后给出的评论。（附我的 Win10 升级 1903 后的桌面截图）
2019-09-11 00:00:00 发布
[3/3] 我这篇论文写得太好了，太重要了，目测将颠覆该理论诸多专家的认知。我用一页半纸才严格证明的一个结论当年在 Milner 的论文里竟然只有一行，这里面水有多深他当时肯定没看出来。我现在就等 Sangiorgi 三天内看了这个证明以后给出的评论。（附我的 Win10 升级 1903 后的桌面截图）
田春冰河
2019-09-03 00:00:00 发布
[1/3] 昨天提交给 HOL 的 PR 已经被快速合并了，我在所有代码贡献者里按新增代码行数仍然排名第7，但已经以7000多行的优势把前不久刚刚超越的第8名 Ramana Kumar 甩在后面了。下一个目标是排名第6的 Joe Hurd——概率论形式化的先驱；再往前是 Mike Gordon，已故 HOL 创始人——他已经不可能再写了。
2019-09-03 00:00:00 发布
[1/3] 昨天提交给 HOL 的 PR 已经被快速合并了，我在所有代码贡献者里按新增代码行数仍然排名第7，但已经以7000多行的优势把前不久刚刚超越的第8名 Ramana Kumar 甩在后面了。下一个目标是排名第6的 Joe Hurd——概率论形式化的先驱；再往前是 Mike Gordon，已故 HOL 创始人——他已经不可能再写了。
田春冰河
2019-09-02 00:00:00 发布
[2/3] 我今天一鼓作气，终于彻底完成了 CCS 进一步形式化工作（本质上就只有两个新定理），因为后期出了错误不得不回炉好几个引理的证明，比预计的进度晚了两天。核心代码 4000 多行，还优化了的一些旧定理的证明，所有代码作为一个巨大的 PR 刚刚已经发给 HOL 官方了。网页链接
2019-09-02 00:00:00 发布
[2/3] 我今天一鼓作气，终于彻底完成了 CCS 进一步形式化工作（本质上就只有两个新定理），因为后期出了错误不得不回炉好几个引理的证明，比预计的进度晚了两天。核心代码 4000 多行，还优化了的一些旧定理的证明，所有代码作为一个巨大的 PR 刚刚已经发给 HOL 官方了。网页链接
田春冰河
2019-09-02 00:00:00 发布
[1/3] 上周五提到的 “重大发现”…… 后来证明是我错了。Milner 关于强互模拟方程组唯一解定理的那个证明其实是正确的，但有一个关键步骤需要针对 “方程” 的定义略加修改。我后来反复探索，最后终于找到了有针对性的修复证明的方法。所以并没有什么重大发现，但这个工作本身已经可以写进论文了。
2019-09-02 00:00:00 发布
[1/3] 上周五提到的 “重大发现”…… 后来证明是我错了。Milner 关于强互模拟方程组唯一解定理的那个证明其实是正确的，但有一个关键步骤需要针对 “方程” 的定义略加修改。我后来反复探索，最后终于找到了有针对性的修复证明的方法。所以并没有什么重大发现，但这个工作本身已经可以写进论文了。
田春冰河
2019-08-29 00:00:00 发布
[3/3] SBCL 维护者（有些是 Google 员工）太牛逼了，几天功夫就成功移植到 64 位 PowerPC 上了，而且是 big/little endian 两个版本，这一下就把 Clozure CL 压下去了。Lisp 平台维护者这种深入到各种体系结构底层的编程能力实在令人羡慕，这跟我这种只会写写纯 Lisp 的 Lisper 是截然不同的两种人。
2019-08-29 00:00:00 发布
[3/3] SBCL 维护者（有些是 Google 员工）太牛逼了，几天功夫就成功移植到 64 位 PowerPC 上了，而且是 big/little endian 两个版本，这一下就把 Clozure CL 压下去了。Lisp 平台维护者这种深入到各种体系结构底层的编程能力实在令人羡慕，这跟我这种只会写写纯 Lisp 的 Lisper 是截然不同的两种人。
田春冰河
2019-08-22 00:00:00 发布
[2/3] 你看，活人终归是不能让尿憋死。我从 GitHub 上把 Aquamacs 的源代码 clone 下来，然后就花了半个小时就轻松编译完了，然后运行起来一点儿问题没有。要想同一个程序兼容多种操作系统版本，就一定要在所支持的最老的那个版本里构建用于发布的软件包，Windows/Linux/Mac 下都是这样。
2019-08-22 00:00:00 发布
[2/3] 你看，活人终归是不能让尿憋死。我从 GitHub 上把 Aquamacs 的源代码 clone 下来，然后就花了半个小时就轻松编译完了，然后运行起来一点儿问题没有。要想同一个程序兼容多种操作系统版本，就一定要在所支持的最老的那个版本里构建用于发布的软件包，Windows/Linux/Mac 下都是这样。
田春冰河
中国素质教育的典范
| 50 | 30445 | 5044 |
| 关注 | 粉丝 | 微博 |