抜け落ちの保証はないコンピュータの数え上げ

ブライアンデイビスの論説で取り上げられた3番目の項目です．複雑な数え上げのような問題は，コンピュータ支援で解いても，それですべてという証明は困難．数学の証明の完全性は追及できるのか．
事例に，ディビスは，有限単純群の分類のテーマを取り上げていますが，
ディビスも初めに述べているように，有限単純群や群論に深入りはしませんので，この論説の主題はこれらの知識がなくても理解できます．

とはいうものの，多少の背景概念があると理解に役立つので，短い乱暴な解説を訳者はここで加えようと思います．（中途半端な解説で我慢してください．いずれ結晶点群や空間群を例にして群の構成の話はするつもりです．群や正規部分群とは何かはそれまでお預けで話を進めます）
■単純群とは，自明な正規部分群以外の正規部分群を含まない群で，自然数で言えば素数のようなものです．有限群を単純群の積に分解するのは，自然数では素因数分解のイメージです．
デイビスの論説の主題となっている有限単純群の分類は，以下の定理になっています．
（定理）有限単純群は次のいずれかと同型である．
１．素数位数の巡回群
２．5次以上の交代群
３．Lie型の単純群
４．26個の散在型単純群
１～３は系列ですが，どちらの系列にも属する群も存在し，この分類は重複を許すものです．４は系列に属さず存在する群なので散在型と呼ばれます．モンスター群は散在型単純群に分類されます．
デイビスの論説の趣旨は，この定理のような数え上げの問題は証明完了と保証できないと言いたいのです．

この分類定理は，10年を越える500以上もある論文を繋ぎ合わせて得られた結論ですが，論理の繋ぎ目にギャップがある可能性はあり．分類に抜け落ちがないとは言えません．理論全体を理解している人は10人いるかどうかということで，今後とも証明が完全であることの証明ができるかどうかは疑わしいと言うことです．それでは，デイビスの論文（続３）を読みましょう．

ーーー

■数学は何処へ行く（続３）， Brian Davies（ロンドンキングスカレッジ）

https://elementy.ru/nauchno-populyarnaya_biblioteka/164681/164685

これから説明する3番目の危機も、不必要な複雑さに関連していますが、ある意味ではもっと深刻です。この場合、私たちはコンピュータは使いませんが、「純粋数学」におけるコンピュータの証明が容認できない理由です。私が提供する例は、現代数学の中心的な分野の1つである群論に関連します。

1970年代に、100人を超える群論専門家が一種のコンソーシアムを結成し、単純な有限群の完全な分類を目標にしました。この問題は非常に骨の折れるものとして提起され、その解決策は、純粋数学で「フロー法」と「分業」を使用した唯一の例です。ダニエル・ゴレンシュタインの指導の下で、問題は「パッケージ」に分解され、世界中の数学者のさまざまなグループに割り当てられました。10年間の集中的な作業の後、3つの可算無限の系列族と、26個の散在型で構成されるすべての有限単純群の完全な分類をまとめることに成功しました［訳注）約500編の論文］。 「モンスター」と呼ばれる最高位数の散在型の存在は、コンピューターの助けを借りてのみ証明することができました。 幸いなことに、この問題をめぐる危機は、群分類の詳細に立ち入ることなく議論することができます。有限単純群が何であるかを知る必要さえありません。

1980年代には、群分類自体と同じくらい興味深いことが起こりました。外向きのポジティブな変化です。コンピューターを使わずに「モンスター」の存在を証明する方法の発見です。さまざまな数学者グループの努力を組み合わせて、模索された証明の大規模な研究を実施することが決定されましたが、期待される結果の代わりに、以前に受け入れられた証明の多くのギャップが特定されました。ほとんどの穴にはパッチが適用されていましたが、1990年に単純な有限グループの完全な分類が得られたという記述は時期尚早であると見なされるほど、深刻であることが判明しました。時が経つにつれて、このギャップはアシュバッハーとスミスの証明で埋められ、再びその証明は非常に正しいように見えました[3]。この最終的な証明の20巻のうち、これまでに公開されたのは不完全な5巻だけであり、これは定理が「証明」されてから四半世紀後のことです。詳細については、[3]、[27]を参照してください。プロジェクトに最も関心のある参加者の1人であるミハエル・アッシュバッハーは、いつの日か新しい有限単純群が発見される可能性を排除していません。
その特性がすでに知られているどれかに関連しているなら、大したことではありませんが，
アッシュバッハーは、根本的に新しい有限単純群である可能性を排除していません。その場合は、分類に関するすべての作業を最初から始めなければなりません [4]。Jean-Pierre Serre は用いられる証明の正しさと完全さに懐疑的であることを記しておきます [24]．

アッシュバッハーは、証明は「外見は十分に強い」と考えています。それは、特定された欠点が、証明のメインラインに影響を与えることなく、適度な量の追加作業でこれまでに修正できたからです。残念ながら、これは証明が正しいことを意味するものではありません。証明の強さは、そのリンクの最も弱いものによって決定されます。これまで、失敗したリンクが比較的簡単に新しいリンクに置き換えられたという事実は、これが将来何度も成功することを保証するものではありません。

個々のスレッドの切断があるネットワークの形の証明をイメージしましょう。ネットワーク全体の整合性を脅かさないで、どこかにハエが這うのに十分な大きさの穴があることは排除できません。ハエ（この場合は有限単純群）の大部分は捕らえられますが、すべてではありません。

数学的知識を相互に関連する事実のウェブと比較するという考えは、線形論理の役割を減らし、数学的証明の問題を確率論的平面に移します。これは必然的に不必要な複雑な構造につながります。この考えは新しいものではありませんが、数学者自身が向かうのは比較的最近です。同様の類似点は、特にアシュバッはー [4]によって与えられており、「古典的な数学」とは対照的に、データを整理するさまざまな方法が豊富な、情報集約型の科学としての現代の数学と生物学の類似点を示しています。

有限単純群の最終分類案の完成（徹底的な最終報告書を発行するという意味で）に関しては、自然な老齢化で主要な参加者を失ったために危機に瀕しています。さらに10年後、それらのほとんどは生命や数学から消え、分類を完了するのに十分なほど問題を深く理解している科学者は少ないでしょう。しかし、プロジェクトが徹底的な最終報告で終わったとしても、少なくともマルチボリューム証明の主要な行を理解していると主張する権利を持っている数学者は、おそらく世界に10人もいないでしょう。

したがって、次のような状況になります。数文で定式化された問題の解決には、数万ページのテキストが必要です。証明は完全に書き留められておらず、一貫して書き留められているわけではなく、おそらく書き留められることはなく、最後に、1人の個人が完全に理解することはできません。しかし、得られた結果は重要であり、群理論の枠組みの中でさまざまな問題を解決するために広く使用されていますが、その正確性は依然として大きな問題です。

もちろん、群分類の問題を解決する簡単なアプローチができる可能性もあります。しかし、同じように、これが起こらない可能性もあります。アシュバッハーは、（まだ記録されていない）利用可能な証明の推定全長が過去四半世紀で減少していないという事実を考えると、比較的単純な証明の可能性について懐疑的です。チューリングの研究から、証明が定式化よりも何倍も長い定理があることがわかります。実際、これら2つの長さの比率は任意に大きくすることができます。コーエンは、「中程度に複雑さの数理論の基本問題でさえ、圧倒的多数が合理的な理解を超えている」と確信しています[13]。したがって、将来的には、この種の新しい発見のみが期待できます。