誤ってることが証明済みなら何で今更Leanで検証なんて話になってるの？よくわからんな