データ入力がクソめんどい

囲碁将棋ならAIの出力を棋譜や盤面で表現できるけど、実用的な数学の証明を論理記号の列の形式見せられても人間には解読不能