詳述 · 8件の出来事
AIと数学の歴史
1970年代
Smithsonian National Museum of American History (Wikimedia Commons) · Public domain · Commons ↗ どんな地図も、隣り合う国が同じ色にならないよう4色で塗り分けられる、という定理。1852年に Francis Guthrie が気づいた問いが、1976年にイリノイ大学の Kenneth Appel と Wolfgang Haken によって解かれた。MacTutor（セント・アンドルーズ大学）は、2人が1976年6月21日にコンピュータの助けを借りて証明したと発表したと記している。証明は、約1,500個の「配置」からなる不可避集合をつくり、その一つ一つが可約であることを計算機で確かめるもので、MacTutor によれば可約性の検証に約1,200時間の計算時間を使った。人の手では全体を検算できない証明を証明と呼べるかが論争になり、哲学者 Thomas Tymoczko は1979年に「見渡せない（非通覧的な）証明」として問題にした。1997年に Robertson・Sanders・Seymour・Thomas が633個の配置で組み直した別証明を発表し、2005年には Georges Gonthier と Benjamin Werner が定理証明支援系 Coq で証明全体を機械検証した。
2010年代
Greg L (Wikimedia Commons) · CC BY-SA 3.0 · Commons ↗ 同じ大きさの球を3次元空間に詰めるとき、砲弾を積み上げる面心立方の並べ方より密にはできない ── 1611年に Kepler が書いたこの予想は、1998年8月に Thomas Hales と Samuel Ferguson が膨大な計算機計算を含む証明を発表したことで解かれた。しかし Annals of Mathematics が任じた12人の査読団は計算のすべてを確かめきれず、George Szpiro によれば2002年7月に「99%確か」と報告するにとどまった。証明は2005年に Annals に載ったが、Flyspeck 論文は査読者の完全な認証なしに出版されたと書いている。Hales は2003年1月、証明を定理証明支援系で形式化する Flyspeck 計画を発表し、2014年8月10日に完成した。HOL Light と Isabelle を組み合わせ、2万3,000個超の非線形不等式の検証には Microsoft Azure 上で約5,000プロセッサ時間を使った。正式な報告は2017年5月29日に Forum of Mathematics, Pi に掲載された。
2020年代
MartinThoma (Wikimedia Commons) · CC0 · Commons ↗ Google DeepMind とニューヨーク大学の研究者が2024年1月17日に Nature で発表した、平面幾何の定理証明 AI。2000〜2022年の国際数学オリンピック（IMO）から集めた幾何30問のうち、競技の制限時間内に25問を解いた。従来の最高手法（Wu の方法）は10問、IMO 金メダリストの平均は25.9問（DeepMind の発表）だった。補助線や補助点を提案するニューラル言語モデルと、記号的な演繹エンジンを組み合わせた「ニューロシンボリック」方式で、人間の解答例を使わず、ランダムな図から合成した1億件の定理と証明だけで学習した。出力は人が読める証明で、コードとモデルは公開された。一方、2024年4月の別の研究は、改良した Wu の方法と組み合わせれば記号的手法だけで21問に届くと示し、比較の基準を問い直した。2025年2月の後継 AlphaGeometry2 は、過去25年の IMO 幾何問題の84%を解いたと報告している。
International Mathematical Olympiad (Wikimedia Commons) · Public domain · Commons ↗ Google DeepMind は2024年7月25日、強化学習で形式証明を探す AlphaProof と、幾何専用の AlphaGeometry 2 を組み合わせたシステムが、英国バースで開かれた第65回国際数学オリンピック（IMO）の6問中4問を解き、42点満点中28点を得たと発表した。この年の金メダル基準は29点で、28点は銀メダルの上限にあたる。採点はフィールズ賞受賞者の Timothy Gowers と、IMO 2024 問題選定委員長の Joseph Myers が IMO の基準で行った。AlphaProof は、大会で最も難しく人間の参加者609人中5人しか解けなかった問題を含む3問を、AlphaGeometry 2 は幾何の第4問を解いた。ただし問題は人手で証明支援系 Lean の形式言語に翻訳され、1問は数分で解けたが他は最大3日かかった。人間は4.5時間の試験を2回受ける。手法の論文は2025年11月に Nature に載った。
