>>989
漫然とインプットデータといわれても困る

公理や定理の式が正しいとして、証明が間違っていたら？ということはない

公理や定理の式が間違っていたら？　それは検証系で検査できることではない

プログラム検証のV&Vで、
後のV(verification　検証)は機械的にできるが
前のV(varidation　妥当性確認）は機械で実施するものではない

https://www.ipa.go.jp/files/000036457.pdf