数学の「＝」（等しい）とはどういうことか？　英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：このコーナーでは、2014年から先端テクノロジーの研究を論文単位で記事にしているWebメディア「Seamless」（シームレス）を主宰する山下裕毅氏が執筆。新規性の高い科学論文を山下氏がピックアップし、解説する。X： ＠shiropen2