今週はわずかにキューを縮めることができた、来週も引き続きやっていきたい
「もう一つ、チェックの難しい証明の例を挙げます。群論のファイト―トンプソンの定理(奇数位数定理)の証明です。(中略)この定理の証明を形式化し、Coq/SSReflectで完全にチェックしました。すべての証明を記述するまでにかかった労力は、15人がかりで7年と言われています」(『Coq/SSReflect/MathCompによる定理証明』より)という記述を見て人月に換算しそうになってしまったの本当につらい
このアカウントは、notestockで公開設定になっていません。
このアカウントは、notestockで公開設定になっていません。