形式的証明したい - prololo’s diary

証明をバッチリ形式的に書くと、その証明には”正しい”推論しか使われていないことをコンピュータに検査してもらえる。つまり、「定理を乱用してない？」とか、「場合分けに抜けはない？」とか、「『明らか』と書いた部分が実は明らかじゃないのでは？」みたいな悩みから抜け出せる。最高ですね。

証明を機械的に検査する環境（証明支援系, proof assistant）はたくさんあって、CoqとかAgda、Isabelleなんかが有名なんじゃないかと思う。僕は全然詳しくないので

を見て、たくさんあることを知った。

まあ、そんなたくさんある証明支援系のなかで、Microsoft Researchの人たちが作っているLEANをこれから使っていきたい。LEANは一年前くらいにも使っていて、親しみがある。そしてロゴがかっこいい。もう使い方忘れてるのでチュートリアルを通してみて改めてマスターしていくつもり。

今日はLEANの環境が今のPCに入っていなかったから

をみてイントールした。

できれば毎日さわって、ゲーデルの不完全性定理を証明したい。