>>178

だから形式証明なんかほとんどの数学者は必要としてないんだって。
手軽に出来るならケアレスミスのチェック用に便利っていうだけ。
だけど手軽になんか出来ないだろ。