「AIと数学」Part 1 「2026年に起きたこと」資料集
このページは、セミナー「AIと数学」Part 1 「2026年におきたこと」の資料をまとめたものです。画像をクリックすると資料のページが開きます。
これらの編集作業は、マルレクのコンテンツをよりアクセスしやすく、利用しやすいものにしようという 「MaruLabo KnowledgeHub プロジェクト(MKHP)」の一環として行われています。
2026年におきたこと
僕は、AI技術は、
AI-1 ： 「 大規模言語モデル＋α 」から
AI-2 ： 「 大規模言語モデル＋形式的証明システム＋α 」へ
と発展・進化していると考えています。この変化の中心舞台が、AIと数学の領域です。
AIと数学の領域の現状を知るうえで、先日OpenAIが公開した"Ten Advances in Mathematics and Theoretical Computer Science（「数学と理論計算機科学における10の進展」）" という論文は重要なものです。OpenAIは、10個の数学の問題すべてに対するlean上での「形式的証明」を、GitHubで公開したことに注目しています。
この論文の登場によって、AIと数学の領域では、AIはLLMベースの生成AIから、Neuro+Formal ベースのAIに急速に進化・発展していると考えることが出きると思います。この変化は、重要です。
Ten Advances in Mathematics and Theoretical Computer Science
How the Ideas Came Together
Theorem Proving in Lean 4
数学コミュニティからの「ライデン宣言」
「いかにしてAIが数学をだめにするのをふせぐか」(blog)
「人工知能と数学に関するライデン宣言」日本語訳 (blog)
変化の理論的起源に遡る
OpenAIは、すでに2022年にAIに形式的証明を実行させようとした"Theorem Prover" という取り組みを行っていました。ただ、この分野での急速な進化を、この4年間の発展で説明するのは、不十分だと僕は感じています。
こうした変化の背景を考えるうえでは、一見するとAIとは無関係に思えるかもしれませんが、AI技術の外で、数学、コンピュータ・サイエンスの内部で先行した、大きな変化に注目する必要があると思います。それは、次の二つです。
- 2010年代のVoevodsky の数学でのコンピュータ利用についての先駆的取り組み
- 2020年のコンピュータ・サイエンスでのMIP*=RE 定理の発見
今回のセミナーは、こうした視点から、現在の到達点を考えていこうというものです。
コンピュータ・サイエンスの現在 「はじめに」
基本的な論文
The Origins and Motivations of Univalent Foundations
A Personal Mission to Develop Computer Proof Verification to Avoid Mathematical Mistakes
Univalent Foundations and the Large-Scale Formalization of Mathematic
MIP*=RE
「AIと数学」マルレクの関連セミナー
2019/11/28 「IT技術とCoqの世界」
2020/11/27「コンピュータ・サイエンスの現在 — MIP*=RE定理とは何か？」
2020/12/25「MIP*=RE 入門」
2022/03/26「コンピュータ、数学の問題を解き始める」
2024/08/31「コンピュータと数学」
「AIと数学」セミナーに向けたblog
このblogの基本的な時間軸
- 2013年：VoevodskyのUnivalent Foundation
- 2020年：MIP*=RE
- 2022年：OpenAI "Theorem Prover"
- 2026年：OpenAI ""Ten Advances in Mathematics ..."
コメント
コメントを投稿