｜リーンで「正しくない」

現在の証明支援系は、ある命題が他の命題たちから
導出できるかそうでないかだけを判定します。