コンピュータによる将棋やチェスなどの知見を、定理の自動証明に
も適用できるのではないだろうか。過去の証明を沢山放り込んで
パターンを学習させることで、未知の命題が試行錯誤により、より良く
解けたりしないかな。
　特に、正しい命題の場合には、いってみれば詰め将棋のようなものだから、
どうだか分からない命題よりは易しいのではないだろうか？