著名な数学者テレンス・タオは、AIの進歩により数学が「証明不足」の時代から「証明過剰」の時代へと移行していることを指摘しています。大規模言語モデル（LLM）は急速に証明を生成し、Leanのようなツールは検証を自動化しています。しかし、これらの証明を人間が理解する能力は遅れており、「インピーダンスミスマッチ」が生じています。タオはエルデシュ問題を例に挙げ、学生がChatGPTを使って80分で証明を生成した一方で、彼自身はそれを検証し理解するのに24時間かかり、その過程で新たなつながりを発見したと述べています。 タオは、証明を生成することよりも理解することが希少な資源となるため、学術評価システムの再構築が必要になると予測しています。彼は、数学の未来は単に証明を作成するのではなく、適切な問題を選び、検証し、結果を消化する能力に焦点が当てられると強調しています。この変化は、理論物理学や暗号学などの他の証明に基づく分野にも影響を与えると期待されており、AIが数学研究の風景を変え続ける中で重要な意味を持つと考えられています。