1: ネギ速の名無しさん 2026/05/31(日) 10:48:00.62 ID:PSsXu4F+0 Google DeepMindは2026年5月、大規模言語モデル（LLM）と定理証明支援系「Lean」を融合させた形式証明探索AI「AlphaProof Nexus」を発表した。本システムは、LLMの生成した証明ステップをLeanで厳密に検証し、エラー修正を繰り返すことで、ハルシネーションを排した絶対的に正しい証明を自律的に構築する。本AIは、56年間未解決だった2件を含むエルデシュ問題9件や、未解決予想44件を解決した。異なる数学領域を結合させる独創的な解法は数学者からも高く評価され、1問あたりの推論コストは数百ドルに抑えられた。▼ ▲ 閉じる同時期にOpenAIのAIも別のエルデシュ問題を解決しており、AI開発競争が数学の難問解決という形で表面化している。この成果は、数学研究にパラダイムシフトをもたらした。これまで天才のひらめきに依存した数学的発見が計算リソースで管理可能になり、AIが問題定義の誤りすら修正し、人間は高次元の概念探求に集中するという新たな協調関係が生まれつつある。一方で、AIによる証明の量産は既存の査読システムを機能不全に陥らせ、発見者のクレジットを巡る論争を招くなど、学術コミュニティに制度やルールの再考を強く迫っている。 【さすがのグーグル】GoogleDeepMindの数学AI、50…Google DeepMindは2026年5月21日、AIを用いた形式証明探索システム「AlphaProof Nexus」に関する論文を公開した… - www.sbbit.jp 2: ネギ速の名無しさん 2026/05/31(日) 10:48:11.67 ID:CZ1engfe0 長くて読めない 3: ネギ速の名無しさん 2026/05/31(日) 10:50:12.47 ID:BB1tuKsSd 人はもう終わりということ…