AIの証明が「100%正しい」と判定できる仕組み

確定申告もLeanのコンパイルみたいに一瞬で終わるようになってほしいのだ！ （僕のずんだ餅の領収書は型エラーで弾かれそうなのだ…） ⏱️ チャプター 00:00 AI数学界の大騒動 03:43 人間の査読の限界 06:57 プログラムの型と数学の証明 11:20 Leanの仕組みとAIの相性 17:43 ナビエ・ストークス問題とリーマン予想の真相 20:44 AI時代の数学の未来 🔬 主なトピック・キーワード ・ミレニアム懸賞問題 　- ナビエ・ストークス方程式 　- リーマン予想 　- 準リーマン予想 ・四色定理 ・ケプラー予想 ・フェルマーの最終定理 ・査読 ・カリー＝ハワード同型対応 ・型システム ・型エラー ・コンパイラ ・Lean 4 ・mathlib ・公理 ・タクティクス ・論理カーネル ・Comparator ・nanoda ・ハルシネーション 📜 音声・キャラクター・音楽クレジット 【音声合成】 ・VOICEVOX:ずんだもん ・VOICEVOX:四国めたん 　https://voicevox.hiroshiba.jp/ 　音源利用規約：https://zunko.jp/con_ongen_kiyaku.html 【キャラクター・立ち絵】 ・立ち絵：坂本アヒル 様 　ずんだもん：https://seiga.nicovideo.jp/seiga/im10... 　四国めたん：https://seiga.nicovideo.jp/seiga/im10... ・パーツ展開元：NightWork「四国めたんとずんだもん シェル」 　https://nightwork.sakura.ne.jp/ukagak... ・キャラクター権利元：© SSS LLC.（東北ずん子・ずんだもんプロジェクト） 　https://zunko.jp/ 【BGM】 ・shuffle shuffle — KK 様 　作者配布ページ：https://note.com/kk1_/n/n0fe662348552 　ニコニ・コモンズ：https://commons.nicovideo.jp/material... 　※動画への使用にあたり、音量調整・ループ処理・フェードによる尺調整を行っています。 📚 引用・使用資料クレジット（画像・写真・論文・参考資料） CCライセンス等の画像は動画内の枠に合わせて縮小・トリミングしています。CC BY-SAの改変部分は同じライセンスで提供します。 【クリエイティブ・コモンズ表示（CC BY / CC BY-SA）】 ・ケヴィン・バザード肖像（2007）：Paula Buzzard / CC BY-SA 3.0 　https://commons.wikimedia.org/wiki/Fi... ・ウィリアム・A・ハワード肖像（2004）：Andrej Bauer / CC BY-SA 2.5 si 　https://commons.wikimedia.org/wiki/Fi... ・テレンス・タオ写真（2026 IPAM）：IPAM / CC BY 4.0 　https://commons.wikimedia.org/wiki/Fi... ・国土数値情報（行政区域データ N03、国交省 / CC BY 4.0）：https://nlftp.mlit.go.jp/ksj/gml/data... 　※市区町村境界を結合・簡略化し四色定理の地図として加工・着色。 ・Wiktionary “lean” 定義：Wiktionary contributors / CC BY-SA 4.0 　https://en.wiktionary.org/wiki/lean 【パブリックドメイン・著作権表示】 ・アンドリュー・ワイルズ肖像（2005）：copyright C. J. Mozzochi, Princeton N.J 　https://commons.wikimedia.org/wiki/Fi... ・ハスケル・カリー肖像（1920）：Public domain 　https://commons.wikimedia.org/wiki/Fi... ・ベルンハルト・リーマン肖像（1863）：Public domain 　https://commons.wikimedia.org/wiki/Fi... ・郵便メーター印「FOUR COLORS SUFFICE」（1976）：Smithsonian NMAH 所蔵 / Public domain 　https://commons.wikimedia.org/wiki/Fi... ・リーマン 1859年論文（素数の個数について、ベルリン・アカデミー）：Public domain 　https://commons.wikimedia.org/wiki/Fi... 【使用論文・プレプリント】 ・A. Bastounis et al., “Navier-Stokes lost in translation…” arXiv:2610.08144 (2026). 　https://arxiv.org/abs/2610.08144 ・OpenAI, “FINITE TIME BLOWUP FOR NAVIER–STOKES” (2026). 　https://cdn.openai.com/pdf/32d9f210-8... ・OpenAI, “The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane ℜs ＞ 7/8” (2026). 　https://github.com/openai/math/blob/m... ・T. C. Hales et al., “A formal proof of the Kepler conjecture,” arXiv:1501.02155 (2015). 　https://arxiv.org/abs/1501.02155 ・L. de Moura et al., “The Lean Theorem Prover (system description),” CADE (2015). 　https://lean-lang.org/papers/system.pdf ・T. Klowden, T. Tao, “Mathematical methods and human thought in the age of AI,” arXiv:2603.26524 (2026). 　https://arxiv.org/abs/2603.26524 【オープンソース・公式リソース・参考資料】 ・Lean 公式サイト：https://lean-lang.org/（ロゴ商標：/logos/） ・書籍『Theorem Proving in Lean 4』：https://lean-lang.org/theorem_proving... ・Lean 4 本体：https://github.com/leanprover/lean4 (Apache-2.0) ・Mathlib 4：https://github.com/leanprover-communi... (Apache-2.0) ・Comparator：https://github.com/leanprover/comparator (Apache-2.0) ・独立型チェッカー nanoda_lib：https://github.com/ammkrn/nanoda_lib ・Anthropic「Formalizing Fermat’s Last Theorem」：https://www.anthropic.com/research/fo... ・Anthropic FLT形式化：https://github.com/anthropics/fermats... ・OpenAI ナビエ・ストークス形式化：https://github.com/openai/NavierStoke... ・OpenAI 数学論文・形式化：https://github.com/openai/math ・Kevin Buzzard「The Xena Project」：https://xenaproject.wordpress.com/ ・Terence Tao ブログ：https://terrytao.wordpress.com/ ・Terence Tao Mathstodon投稿：https://mathstodon.xyz/@tao/116789374... ・PFR予想ブループリント（Terence Tao ほか）：https://teorth.github.io/pfr/ ・四色定理 Coq形式化：https://github.com/rocq-community/fou... (CeCILL-B) ・ケプラー予想 Flyspeck：https://github.com/flyspeck/flyspeck