新一の「心の一票」

​前回の記事​では、定理証明支援系ソフトLeanに関連した活動が昨年後半、（私を含め）私の周辺において益々活発になっていることについてご報告しましたが、今回の記事では、少なくとも私の現在の認識において、このような活動に関わることにどのような意義があるかについて検証し、解説していきたいと思います。

ただし、誤解がないように明記しておきますと、「活動に関わる」と言っても、私自身はこれまでそういう計算機のプログラミングの世界とは全く縁がなかったですし、今でも私自身が直接プログラムのコードを書く立場ではなく、専門家がコードを書けるように、数学的な理論の整理の仕組みを考え直したりして、関連した資料の作成やメール上の議論を通して数学側からコードを書く業務のお手伝いをする立場です。つまり、これまでのように、人間の数学者ではなく、（直接コードを書く立場の専門家を介して）いわば計算機を相手に自分の研究を解説することによって様々な新たな数学的知見を獲得する機会に恵まれ、数学者としても非常に有意義な刺激を得ているということです。

論理構造の記録装置としてのLeanの活用について

Leanの活用方法として通常想定されるのは、数学的証明の正否、つまり数学的証明が本当に正しいかどうかを確認するための技術としての活用です。昨年10月に公開した報告書​[Rpt25]​の§3.1でも解説している通り、私はこのような正否の確認装置としてのLeanの使い方・捉え方には特に反対するわけではなく、他者がそういう観点から宇宙際タイヒミューラー理論の形式化を捉えることに異を唱える立場ではないですが、一方で、宇宙際タイヒミューラー理論の場合、理論を取り巻く特殊な社会的・政治的力学を考慮すると、私としてはちょっと違う方向性の活用の仕方に注目しております。

宇宙際タイヒミューラー理論の場合、大量の、不適切な内容の報道や、ネット上のつまらない雑音等により、途轍もなく難解かつ複雑怪奇な理論であるというイメージが、残念ながら多くの数学者の間では定着していますが、多くの数学の理論と同様、適切な予備知識（＝宇宙際タイヒミューラー理論の場合、数論幾何や遠アーベル幾何ということになるが）を有する研究者が普通に適切に勉強すればそれほど難しい理論ではありません。このような実態があるからこそ、​[EssLgc]​§1.12でも指摘していることですが、実際に形式化に関わっている研究者からも、（形式化には別に意味がないということにはならないが）理論の特に難解と言われている部分の形式化が完了したとしても、実態は簡単過ぎてみんながっかりするのではないかという趣旨の声が度々聞かれます。

因みに、数学界での、様々な実態と乖離した情報の拡散によって作り上げられてしまっている差別的な閉塞感・門前払い感と比較すると、多くのLean関係者と交流していると、雲泥の差と称して差し支えない位の、別世界級の清々しい空気感があって、簡単に要約すると、

　　理論の数学的内容は知らないし余り興味
　　がないが、寧ろLeanの技術的性能・優位
　　性を発揮する舞台・好機として捉えられ
　　認識されている、宇宙際タイヒミューラー
　　理論の形式化業務に対しては、常に前向き

　　で開かれた、積極的かつ建設的な姿勢で
　　対応する

という態度が昨年経験したことの中でも、最も印象的かつ特筆すべきものの一つでした。

少し脱線してしまいましたが、元の話題に戻りますと、これまでの15年程の、宇宙際タイヒミューラー理論を解説する経験を踏まえて総括すると、理論を勉強する上において最も本質的な「難点」・「障害」となるものは、寧ろ

・これまでの多くの報道やネット上の雑音から拡散される、実態と乖離したイメージ、それから

・理論が多くの数学者がこれまで経験している数学とだいぶ違う方向性の議論から成り立っていること

に起因すると思われる、

　　勉強する側の人間の（実際には事実無根の）
　　様々な一方的な想定や先入観と相性の良い
　　展開が演出されるように、理論を勝手に
　　改変した上で、元々の理論と論理的関係性
　　のない、理論の改変版の問題点や欠陥を、
　　元々の理論のものであるかのような、虚偽

　　の主張を振りかざす誘惑に抗うことができ
　　ず、勝手にそのような路線に暴走してしまう

傾向があることです。

これは、別の言い方をすると、深刻な知財権侵害に当たる言動であり（詳しくは​[EssLgc]​§1.10をご参照いただきたい）、この事象については、

・​[EssLgc]​全体を通して取り上げているRCSの主張（＝テータ・リンクあるいはログ・リンクの両側にある数学的対象の同型なコピーを同一視しても理論の論理構造への影響はないとする主張）、

・​[Rpt24]​で取り上げられているプレプリント・シリーズ、

・​[Rpt25]​の§1, §2で取り上げられている、某科学記者に書かれた記事

は典型的な事例として挙げられます。更に、昨年後半、理論の形式化に関する議論を、Leanの専門家と進める上においても、Leanに関する技術的な問題という面においてはこれまでの事例と違うものの、再び同様の事象が見られました。（これについては、以下の「species/mutations」に関する解説をご参照いただきたい。）

​[Rpt25]の§1や§3で解説している通り、上記の諸々の事例に共通しているのは、問題となっている虚偽の主張が、査読による審査体制が適切に機能している、国際的に認められた数学雑誌で出版されている論文ではなく、ネット上に勝手に公開された原稿や書き込みで展開されている点です。本ブログでも度々引用しているヨーロッパ数学会EMSの行動規範​[EMSCOP]​の「著者の責任」第6条にも書かれている通り、

　　　著者が新しい数学的主張を発表する際、
　　　その主張の完全な証明を大幅な遅延なく
　　　公開する義務を負う、

という数学研究を遂行する上における基本的な倫理的な義務は、上記のいずれの事例においても、遵守されていないことが基本的な問題であると言えます。これまでの数学界の慣行として、査読付き出版の他にも、研究集会を開くこと等、より多くの数学者による検証を行なうための手段も用意されています。

しかし、査読付き出版や研究集会等、上記のような伝統的かつ「アナログ」な仕組みによる、

　　長期的な検証や説明責任の枠組から外れた
　　主張・原稿が、様々な社会的・政治的力学
　　や「信仰」等（この二者の癒着については
　　以前の​ブログ記事​をご参照いただきたい）に

　　より数学界において罷り通ってしまう場合
　　はどうずればよいか、これがまさに宇宙際
　　タイヒミューラー理論を巡る状況が突き
　　付けている課題

ということになります。

そこで、Leanに対する、通常の考え方と多少違う方向性の活用方法の話に戻りますが、​[Rpt25]§3.1で解説している通り、

　　Leanで書かれたコードは、通常のPDF形式
　　の原稿等と違って、数学的議論の論理構造
　　が、コードのレベルで直接的に記述されて
　　いることにより、長期的に、例えば議論の
　　数学的内容を理解している数学者がもはや
　　この世にいない、数百年後でも、容易かつ
　　直接的にアクセスできるような形で、その

　　論理構造（＝特に論理がちゃんと飛躍なく

　　回っていること）の記録を保存する性能の

　　ある技術である

と言えます。つまり、特にLeanという技術を稼働させられる技術者さえいれば、長期的に（＝例えば数百年後でも）、

　　いかなる理論の改変版でも、元々の宇宙際
　　タイヒミューラー理論との論理的関係性が
　　証明されていないものとして機械的に弾く
　　ことが（少なくとも原理的には）可能

になります。宇宙際タイヒミューラー理論の文脈では、Leanがこのような、長期的検証・説明責任の枠組を提供していることに非常に大きな意義があると考えております。

意思疎通の手段としてのLeanの活用について

一般論として、ある数学的理論の、Leanによる形式化を進める上において、まず優先的に行なうべき作業は、理論の基本的な用語の定義の定式化であると、昨年後半、あるLeanの専門家から聞きました。これは私自身が、元々数学の論文を執筆する上において昔から実践している考え方と整合する考え方であり、宇宙際タイヒミューラー理論の場合、最も基本的な用語・概念は間違いなく、「関手的アルゴリズム」（＝「functorial algorithm」）ということになります。この用語ないしは概念は、本当は、宇宙際タイヒミューラー理論だけでなく、数理研において1990年代半ばから盛んになっている流儀の遠アーベル幾何全般において、非常に基本的な立ち位置にあるものです。

この「関手的アルゴリズム」という概念は、宇宙際タイヒミューラー理論の原論文4編の第4論文[IUTchIV]の§3で解説している「species/mutations」という概念によって定式化されており、つまり、理論の形式化を進める上においても、まずしっかり押さえておきたいのは、「species/mutations」の形式化ということになります。因みに、技術的な詳細に関しては、​[IUTchIV]§3をご参照いただきたいと思いますが、簡単に嚙み砕いて説明すると、

・species（＝「種」）は、集合論的論理式で定義される、「数学的対象の種類」（＝つまり、「群」、「環」、「代数多様体」のようなもの）で、

・mutation（＝「突然変異」）は、集合論的論理式で定義される、あるspeciesから別のspeciesへの変換、つまり構成の手順

ということになります。つまり、「関手的アルゴリズム」というのは、より技術的な用語で表現すると、まさしく「mutation」ということになります。

私自身、2010年～2011年頃、[IUTchIV]§3を執筆したとき、species/mutationは、特に難しい話でもなく、取り立てて新奇性のある話でもなく、多くの数学者が当たり前に脳内で無意識のうちにこなしている処理を、（同様の概念が明示的に記述されている適切な文献が見付からなかったために）ただ自分で明示的に記述してみただけのものに過ぎないという認識でした。また論文を公開した2012年以降も、何名かの基礎論の専門家にも目を通していただいていますが、みんな口を揃えてまさしく特に新奇性のない、当たり前なことしか書かれていないという趣旨の評価や総括をしています。いずれにしても、自分自身、まさにそのように考えていたからこそ、宇宙際タイヒミューラー理論を理解する上で障害となり得る側面であるという認識はこれまで全くなかったです。

一方で、species/mutationの、Leanによる形式化の可能性について調べ始めた途端、全く想定外の展開に見舞われてしまいました。まず、species/mutationの定義では、集合論的な（＝つまり、いわゆるZFCの）論理式が非常に中心的な役割を果たしますが、これまでのLeanの標準とされているライブラリMathLibでは、ZFCモデル（＝つまり、標準的な集合論のモデル）は用意されているため、特定の集合に対する特定の論理式をLean上で扱うことが可能となっていますが、一方で、species/mutationの理論において本質的な役割を果たす「不定元のような論理式」（＝特定されていない、「とある論理式Φ」のようなもの）を扱うには、一階述語理論としてのZFCが必要であり、それはMathLib上ではまだ掲載されていないということが判明しました。

ただし、後で分かったことですが、偶々ですが、日本のある若手研究者は一階述語理論としてのZFCの形式化を既に実行しており、それはMathLib上では（MathLibの運営委員会による査読を経ていないため）掲載されていませんが、日本の若手研究者の（大きな仕事ではなく）ちょっとした補足的な仕事としてその形式化が既に実行されているということは、形式化自体は特にそれほど難しい作業ではないということです。

しかし、これが逆に非常に不思議な発見のように思われました。つまり、一階述語理論としてのZFCは、数学全体において余りにも重要かつ基本的な理論であり、かつその形式化作業は技術的にはそれほど困難なものでもないにも関わらず、MathLib上ではそれが未だに行なわれていないというのは、かなり不思議な状況のように思われました。言い換えると、それは

　　　一階述語理論としてのZFCの形式化は、