Innovative Tech

数学の「＝」（等しい）とはどういうことか？　英ICL教授が発表　「コンピュータの登場で定義が曖昧に」

　英インペリアル・カレッジ・ロンドン（ICL）の教授であり、数学者のケビン・バザードさんの単著論文「Grothendieck’s use of equality」は、数学者が等式の概念をどのように使用しているか、そしてそれが数学の形式化を試みる際にどのような影響を与えるかについて議論した研究報告である。

　バザードさんは「現状、数学者は等式の概念を曖昧に使っており、近年のコンピュータプログラムによる証明（形式化）においてその曖昧さが障害になっている」と指摘する。

　「＝」（等号）にみる一般的な等式の定義は、両辺が同じ数学的対象を表しており、一方から他方への論理的な変換によって証明できるものである（伝統的な等式）。状況が変わり始めたのは、現代数学のほとんどの論理的基礎を提供する集合論が発展してからである。集合論の発展に伴い、等式の新しい定義が導入された。

　それは「2つの集合が同じ要素を含んでいれば等しい」というものである。例えば「1, 2, 3」と「3, 2, 1」という集合は等しい。なぜなら、集合の要素の順番は重要ではないからである。さらに、数学者は2つの集合が同じ要素を含んでいなくても、それらの間に明らかな対応関係（同型写像）があれば等しいと見なすことがある。

　このような等式の曖昧な定義は、数学者が証明を行う際や論文を書く際には問題にならないが（文脈から意味が分かる）、コンピュータを使って証明をチェックする際には問題を引き起こす。コンピュータプログラムは厳密で正確な指示を必要とするためである。

　この問題を解決するために、数学者の中には「数学の基礎を再定義すればよい」と主張する人もいる。等号の概念を統合する試みも始まっているが、数学の基礎を再定義するのは非常に困難を極める。

　一方で、論文著者であるバザードさんは、将来的には、コンピュータ証明の数学ライブラリが充実することで、数学者が等号の厳密な意味を気にせずに済むようになるかもしれないという。数学者がよく分からず直感的な等号の使い方をしたとしても、システムが理解して不備を指摘してくれるようになるからである。

　バザードさんは「コンピュータ支援による形式化が進むことで、数学における等号の概念的問題が解消される可能性がある」と見通している。

Source and Image Credits: Buzzard, Kevin. “Grothendieck’s use of equality.” arXiv preprint arXiv:2405.10387（2024）.

Innovative Tech

2019年にスタートした本連載「Innovative Tech」は、世界中の幅広い分野から最先端の研究論文を独自視点で厳選、解説している。執筆は研究論文メディア「Seamless」（シームレス）を主宰し、日課として数多くの論文に目を通す山下氏が担当。イラストや漫画は、同メディア所属のアーティスト・おね氏が手掛けている。

この連載の記事をもっと見る

この記事の著者

関連記事

• 

  「なぜ時間は過去→未来にしか進まない？」を“量子もつれ”で説明か　未解決問題「時間の矢」に切り込む

• 

  数学の超難問「幾何学的ラングランズ予想」を証明か？　計1000ページ以上の証明論文を米研究者らが公開

• 

  数学の未解決問題「アインシュタイン問題」を“完全解決”する新図形発見　「The hat」を改良

• 

  バッハの曲を数学的に分析　“情報量が多く効果的に伝達している”と判明　米研究者らが検証

• 

  “ABC予想証明”の欠陥発見に賞金1.4億円　ドワンゴ創業者の川上さんが設置