Lean証明の検査迂回

Leanは、数学的な証明をコンピュータで厳密に確認するための定理証明支援系である。

通常は、Leanの中核部分であるカーネルが証明を検査するため、人間の手作業による確認よりも高い信頼性を持つ。

ただし、「Leanで通った」とされる証明を無条件に正しいものとして扱うことはできない。

デバッグ用の設定などによって、本来行われるべきカーネルの検査が迂回される場合があるためである。

そのため、他人のLeanコードを確認するときは、単にエディタ上でエラーが出ていないかを見るだけでは不十分である。

参考