コンピュータが専門ではないので的外れな感想かもしれませんが
こういうものは見たことがないので面白いと思います
QQで似たような会話できるAIと話したこともありましたが
a4さんのとはちょっと違うかもな
本当に自動定理証明に使えるようになれるのなら、論文とかを書いて有名になれるのではないかな