Profile
金具✅ reblogged at 7 years ago
Masanori Ogino omasanori@mstdn.maud.io
「もう一つ、チェックの難しい証明の例を挙げます。群論のファイト―トンプソンの定理（奇数位数定理）の証明です。（中略）この定理の証明を形式化し、Coq/SSReflectで完全にチェックしました。すべての証明を記述するまでにかかった労力は、15人がかりで7年と言われています」（『Coq/SSReflect/MathCompによる定理証明』より）という記述を見て人月に換算しそうになってしまったの本当につらい