18/04/23 18:55:02.71 em4gUmF7.net
・ 一般的に、数学の証明を Coq に書き直すのには大変な労力を必要とするが、
初等的な計算だけで終わっているなら、Coq に書き直す労力は比較的少なくて済むと考えられる。
・ レフェリーが相手してくれなくても、Coq は誰でもウェルカム(なぜなら、Coq はプログラムだから)。
・ いったん証明が Coq に通ったら、その証明は100％正しいことが保証される。もはやレフェリーとか要らない。
・ 5ch の場末のスレッドという、このような場所で賛同者がいくらいても、
社会的には何の価値も無い(まあ現状はここですら賛同者ゼロなんだけど)。
>>1にとってはメリットしかないので、ぜひとも Coq を始めるべき。