イヤ、そっちは「正しく行間読めてないだけ」と反論されて終わり
だからLeanにせよCoqにせよ「証明が正しい」事を示すためには使えるけど「正しくない」事を示すためには使えない
だから正しいと思ってる人専用ツールではある