証明が正しいとされた後に形式化して検証システムにかけたら間違いだったとわかったものも最近あるからなあ