>>641
任意の文字列を確実に検証することを目標にしてるなんて思ってない？
検証ができていないものに対しては「正しくない可能性がある」と考えろ。
形式化が成功していない証明は「未だ証明になっておらず正しくない可能性すらある」と認識すればいいだけさ。