将来的には本当の未解決問題に
自動証明を応用することはありえるのでしょうか？