これ面白い

https://xtech.nikkei.com/atcl/nxt/mag/rob/18/00007/00090/
AI最前線
数学とAI、Terence Taoが語る未来
PFN岡野原氏によるAI解説：第122回
岡野原 大輔 Preferred Networks 共同創業者 代表取締役 最高技術責任者
2025.08.08

　現代最高峰の数学者の一人である米University of California Los Angeles教授のTerence Tao（テレンス・タオ）氏は、数論から偏微分方程式、調和解析、組合せ論に至るまで、幅広い分野で世界的な成果を残してきた。

　その彼が、AIが様々なことができるようになってきた中で、数学でAIをどのように活用できるのかについてLex Fridman氏のポッドキャストで述べている1）。Tao氏は以前より積極的にAIを数学の研究に使えるかを試している。

　ここでは、数学の最前線の分野にAIがどのように使われているのか、今後どのような展望があるのかを通じて、今後のAIがどのように知的作業を必要とする分野で使われていくのかについて論じていきたい。

Lean：定理証明支援系
　AIは文献探索や論文執筆校正など、研究活動で多く貢献しているが、ここでは特に数学に特化した例として定理証明支援を説明する。

　はじめに、数学の分野における形式証明について説明する。今の数学の証明は自然言語と数式で書かれており、言語の曖昧性と、非常に多くの「行間」を読むことによって証明がされている。このような場合、機械的に証明を検証することは難しく、また、証明を支援することも難しい。そのため、形式証明および定理証明支援システムが注目され、その中でも「Lean」が注目されている。

この記事は日経Robotics購読者限定です。次ページでログインまたはお申し込みください。

次ページ
Lean自体はプログラミング言語であるが、数学の..