用 proof assistant/编程语言做数学科研的体验是怎样的？ 第1页

最近形式化验证Odd Order Theorem的团队新出了一本Coq书，

，就是面向不怎么会编程的（但是要会点数学，看了下，至少需要naive set theory，用到点抽代/线代，不过这两可以现用现学），跟会coq的（但是不会他们的库的）读者。

如果会haskell的话，建议看CPDT。

会编程但是不会函数式编程的话，建议看Software Foundation。

数学库的话，基本的底层打齐了（Set, Real, Function, Peano Nat, Category, Abstract Algebra）。。。上一点的有些也有，比如说线代，微积分，都有库，坑点在文档基本上就是源代码的类型/定义pretty print一下。。。导致要什么功能都只能自己爬整个Coq std lib（甚至contrib），比如说我最近在搞Automatic Differentiation，爬了一小时才搞明白大部分的功能在那，然后又爬了一/两个小时才找出div rule。。。如果有人写一个Coq Differential Calculus Tutorial就会好很多。当然，也许问题是不应该直接看Coqdoc而是该load进Coq里面用Coq自带的Search找出来。。。不过一开始的坑过来，读/写Coq pooof的interactiveness，detail不是PDF能比的-这里引的lemma5.6是啥，我直接Check之，甚至不需要一次context jump（而如果paper引的是另外一个paper的lemma，这就不是一个PDF context jump的问题了），没看懂这里的推理步骤怎么办，直接Check proof/debug eauto，现在我该用什么，SearchAbout Rplus derivable就能给出所有跟+，求导相关的定理，paper能做到吗

语言的话，Coq的自动化用好了很爽，有很多现成的decision procedure（Presburger Arithmetic solver，Fourier method for solving inequality，SAT solver，SMT solver，Nelson and Oppen congruence closure algorithm，暴力深搜），你自己也可以任意定制，pattern matching，prolog式backtracking branching，自定义爆搜，自己在OCaml里面写，有不少的时候我自己脑袋里还没证出来，但是Coq已经搞出来了。同时，你做任何的逻辑推导（正向推导，反向推导），coq都会自动的展示出【你还需要证明什么，才能证明整个theorem】，很爽，不需要自己写/放脑袋里。Coq也符合LCF approach-换句话说，只要你在Coq proving mode里面一步步走，到最后把所有东西证明了，就一定对。你也不需要proof read你的证明了，bravo daze!

但是Coq很复杂，甚至有的时候到达了玄学的境界（eauto为什么卡死了，typeclass 推不出来gibberish type error糊多长都可能（因为dependent type，你value有多长type error也能有多长），intuition为什么突然这么慢，说好的LCF approach呢？为啥guarded condition, non structural induction, universe inconsistency（这又是啥？为啥这货跟module相性不好）都不符合LCF approach？par 为啥不solve掉所有goal不能用，simpl刷屏怎么破，exists [].为啥推不出type，自己的tactic不work/太慢怎么debug，type checker termination checker universe checker怎么哄，在线等，为什么tactic变强了反而会break proof，为什么Coq自己有这么多bug（不过别担心，Coq有de brujin criteria，换句话说Coq的proof checker很短，就一百行代码左右，只要这100行没bug就不影响证出来的东西的正确性））。。。诚然，这些问题大部分都能解，但是重点是，不是你今天想用coq check自己的proof，明天就能全速做事，要花很多精力进Coq才能学得好。

另外一点就是自动化太慢，这点完全是Coq自找的。。。因为你每次用Coq check proof，搜索过程都会重新启动，重新搜，不会保存下来。。。设计太美不敢想。不算很严重的问题，比如现在我用了1K行formalize了STLC，然后在证明各种property，process一次大体5分钟，比起人肉验证还是快很多。另：传闻adam的proof要12小时才能check，不过adam是adam，自动化程度高到大部分人都到不了他一半，另外就算如此人肉验证也要12小时以上吧。。。

而，不用自动化的话，的确能去掉绝大部分的玄学，速度也会快很多，但是实在太繁琐。。。当然，可以半自动化半手动化，自己找平衡点，不过这自己也是另外的学问了。

另外还有数学证明中常常跳步，但是Coq中不能跳的问题-正是因为这些跳步导致coq老司机写证明也比纸上写慢。

TLDR：慢，难学，但是能自己写自动化程序，有个助手帮你保存下所有的定理（以供Search），写完了不用担心有问题。同时，也可以只用Coq做一部分工作，剩下的用传统方法做，have the best of both world（自动化程度自己定，跳步直接admit，没库用公理代替，甚至根本不用Coq做证明，字面上证，证完一个定理Coq中admit一个（然后comment中写），只用Coq的Search/Check功能，把Coq当定理library用）。如果你问我得畅不偿失，何尝不花几天自己试下呢？（我是认为肯定够的，不然也不会现在还在用了）

最后打个广告，有个Coq QQ群，300多人左右，活跃度还可以，想学Coq的可以自己搜，人最多的就是了。