記号論理の処理系 + ディープラーニングで、相当数の数学の問題は自動で解けると思うんだが、いまだに実用化されてないってことは、やはり技術的に難しいの？