もっとも見つかりにくいパターン

設定した公理系は無矛盾であったが、実は考えていたものとは違っていた。
しかし、定理の形式的証明ができたので、万事ＯＫと考えた。

その後、実は当初の公理系では強すぎて、排除したいものまで
証明できてしまうことがわかったので、公理系を変えたところ
証明ができなくなった。実際後で反例がみつかった。