leanにはバグがあってそのバグからコラッツ予想を証明した
これを見るに形式化がまだ出来ていないことは確定