自動定理証明が未解決問題をスパスパ解けるようになったら、これは大金持ちになるしかない。