新一の「心の一票」

Calendar

Keyword Search

▼キーワード検索

カテゴリ未分類

(0)

Leanによる形式化は、長期的な検証や説明責任を可能にする記録装置となり得るか？

カテゴリ：研究関連の現状報告

前回の記事では、定理証明支援系ソフト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の形式化は、

形式化の優先順位が余り高くない、

　　　つまり、形式化の優先順位が高いと

　　　されている様々な数学の形式化には

必要ないものであると、Leanによる

　　　形式化に関わっている多くの数学者が
　　　見做している

という状況を物語っているということになります。

因みに、speciesが与えられると、そのspeciesの対象たちからなる「圏」（＝「category」）が定まり、またある二つのspeciesの間のmutationが与えられると、その二つのspeciesが定める圏の間の「関手」（＝「functor」）が定まります。つまり、 species/mutationはcategory/functorという昔からある数学的概念の精密版と見ることができます。一方で、Lean上では、元々、

・「数学的対象の種類」に対応する「type」という概念、それから

・functorに含まれる対応の内容についてある程度具体的な記述が可能な、「dependent functor」という概念

は標準で用意されていますが、type/dependent functorが、species/mutationと決定的に違うのは、集合論的論理式とは無関係であることによって、集合論的な実態のない世界（＝「形式化上の空箱」の世界）のものになってしまうという点です。つまり、本当は通常の純粋数学の研究者の考え方というのは、集合論的な実態のある対象を扱うことを基本とするものであり、その意味では、

species/mutationの方が、通常の

　　　　純粋数学の感覚との相性・整合性

　　　　が、type/dependent functorより

遥かに高い

にも関わらず、Leanの専門家から見ると、不定元のような集合論的な論理式（＝つまり、一階述語理論としてのZFC)を必要とするspecies/mutationsは、これまでのLeanの常識と相容れない方向性のものであり、species/mutationsを導入する代わりに、寧ろtype/dependent functorのみで対応できた方が技術的に楽で嬉しいということになります。

私はLeanの専門家ではないので、深い技術的なことは分かりませんが、上で解説した通り、species/mutationの方が通常の純粋数学の感覚との相性・整合性が、type/dependent functorより遥かに高いということを考慮すると、この際、 species/mutationをLean上で実装し、当たり前に活用できるようにした方が、Leanの、純粋数学の研究者の間での普及を促進する上において、かなり追い風になるのではないかと思わざるを得ません。

更にもう一つの興味深い側面をご紹介しますと、本ブログのこれまでの解説でもそうですが、 [EssLgc] 全体を通して、RCSの問題については、主に論理構造の「∧・∨」（＝「AND・OR」）関連の側面に焦点を当てて解説しておりますが、 [EssLgc] §3.2, §3.8（あるいは [Gate] §2.1）で詳しく解説している通り、その「∧・∨」上の混乱の引き金となっているのは、寧ろまさに speciesと深く関係している問題＝具体的には、貼り合わせデータに登場する群を、

・ある集合論的な設定に登場するただの集合として扱うか、

・体や環への作用という付加構造を備えた群（＝一種のspecies）として扱うか、それとも

・抽象的な群や、モノイドへの作用という付加構造を備えた群（＝これらも、speciesになる）として扱うか、

という問題です。この3択のうち、RCSの「∧・∨」上の混乱の引き金に対応しているのは、「（speciesを無視した）1択目のつもりが、実際には2択目という認識で捉えている」というものであり、元々の宇宙際タイヒミューラー理論に対応しているのは、3択目ということになります。

ここで議論が少し込み入ってしまっているように思いますので、これまでの考察を整理すると、次のような状況になります：

・多くの基礎論の専門家も認めている通り、 species/mutationは全然難しい話でも、新奇性のある話でもない。

・ Leanの専門家は技術的には難しくないことを認めているにも関わらず、species/mutationを用いることを忌避し、これまでの多くの形式化業務でこと足りているtype/dependent functorを用いたがる。

・宇宙際タイヒミューラー理論が難し過ぎて理解できないと主張する数学者の代表格である RCSの混乱の引き金となっているものは、 species的な考え方の無視。

私は昨年後半、上記のような余りにも激しく矛盾している状況、即ち

　　　では、結局、species/mutationは簡単

　　　過ぎて当たり前なものなのか、それとも

　　　宇宙際タイヒミューラー理論が途轍もなく

難解と思われている原因を発生している

　　　張本人なのか？

という状況に接して、深い刺激を受けました。つまり、

・宇宙際タイヒミューラー理論の、多くの数学者から見ての難解さの究極的な原因はspecies/mutation的な考え方が（本当は多くの数学者の脳内の処理では、多くの設定において当たり前に無意識のうちに行なわれているにも関わらず）明示的には認識されていなかったことにあり、かつ

・多くの数学者が、その明示的に認識しない精神状態の下で数学を処理している状況がこれまでの数々のLean形式化に（意図せずして）記録されていた

ということになり、別の言い方をすると、これまで様々な社会的・政治的力学による要因もあって数学者同士の議論では解明が叶わなかった、

　　　宇宙際タイヒミューラー理論の、多く

　　　の数学者から見ての難解さの究極的

　　　な原因を、Leanによる形式化という

　　　技術が、代わりに効率よく炙り出して

　　　くれた

ということになり、Leanという技術の、数学者同士の間の意思疎通の手段＝コミュニケーションのツールとしての威力に強烈な感動を覚えました。

定義と定理の反転

ここで、species/mutationを巡る混乱を炙り出すというLeanの、コミュニケーションのツールとしての威力と深く関係しているもう一つの、数学的にも興味深い現象をご紹介したいと思います。

RCSのspeciesを巡る混乱は、（実際には成り立たない）環論構造のコア性（＝つまり、テータ・リンク（あるいはログ・リンク）の両側のそれぞれの環構造は、一つの環構造として両側で共有されているという性質）を、勝手に成立している性質として扱いたいという（希望的観測のような）願望と深く関係しています。一方で、実際の理論では、最終的には、マルチラディアル表示によって（軽微な不定性を認めるようにすれば）同一の環構造の下でのテータ・リンクの両側の同時的表示は可能になるという趣旨の結論（＝定理）が得られます。つまり、RCSの考え方では、

・同一の環構造の下でのテータ・リンクの両側の同時的表示を勝手に仮定したいという願望（＝定義！）と、

・同一の環構造の下でのテータ・リンクの両側の同時的表示は元々成立しないが、最終的には（適切な調整の下で）ほぼほぼ実現できる（＝定理！）

が引っ繰り返っているということになります。別の言い方をすると、RCSの考え方は、定義と定理の反転によって発生しているものと捉えることができます。

[EssLgc] §1.5でも詳しく解説している通り、19世紀の、複素関数論に対する正しいアプローチは何かを巡る、リーマンとワイエルシュトラスの有名な論争は様々な面において RCSの主張（＝ワイエルシュトラスの主張に対応している）と類似しており、非常に興味深いことに、このリーマンとワイエルシュトラスの論争も、「定義と定理の反転」による論争として捉えることができます。まず、論争の内容を復習しますと、

・ワイエルシュトラスは、複素関数論は、完全に複素平面内の領域上で行なうものであり、

・リーマンが主張していたように、解析接続によって抽象的なリーマン面上で行なうという「荒唐無稽な夢想」のようなことをする必要は本質的にない

という主張でした。一方で、抽象的なリーマン面の理論が更に発展すると、ケーベの一意化定理という（19世紀の基準で言うと）非常に難しく深い定理が証明され、それにより、いかなる（連結な）リーマン面から出発しても、実はその普遍被覆は、（場合によって一点を除けば）複素平面の中に埋め込めることが分かります。つまり、ケーベの一意化定理を認めると、結果的には、同じ複素平面内で全ての（一変数）複素関数論が完結しているという、ワイエルシュトラスが元々主張していたのと同じ状況になりますが、ケーベの一意化定理の非自明性を考えると、「定義と定理の反転」にはかなり著しいものがあります。

こうして改めて状況を整理すると、この「定義と定理の反転」という現象は、前述の「改変の誘惑」と深い関係にあります。つまり、「定義」と「定理」に共通しているのは、

「常識的な感覚で考えると、こう

　　　　　いう状況であって欲しい」

という願望・理想であり、

・非自明な「定理」では、より素朴な、理想から掛け離れた定義・設定から出発して理想的な状況を様々な非自明な考察を通してほぼほぼ実現していくのに対して、

・「定義」では、非自明な考察の展開に付き合う忍耐力が欠如しているため、「最初から理想的な状況が元々実現されている」という認識を一方的に課そうという誘惑に「無条件降伏」してしまいます。

このような文脈において重要な観察ということになるかと思いますが、 Leanによる（宇宙際タイヒミューラー理論の）形式化が完成すれば、上記考察にあったような「改変の誘惑」に一切惑わされたり振り回されたりすることなく、論理構造の処理は機械的に淡々と進むことになります。宇宙際タイヒミューラー理論の場合、多くの数学者は論理構造を処理するのに機械の力を借りなければならないことは様々な意味において残念に思う一方、（まだある側面においては未熟で発展途上にある技術とはいえ）この形式化の技術の到来と実用化が、ぎりぎり私の現役時代に間に合ったこと自体は不幸中の幸いということになるでしょう。

民主主義的価値観と長期的かつ安定的な信頼関係

RCSの主張（＝つまり、テータ・リンクあるいはログ・リンクの両側にある数学的対象の同型なコピーを同一視しても理論の論理構造への影響はないとする主張）の場合、上記議論（や [EssLgc] §3）で検証したような数学的側面もありますが、本ブログでも度々言及している通り、看過してはならない重要な倫理面の問題もあります：

・主張の内容（＝つまり、テータ・リンクあるいはログ・リンクの両側にある数学的対象の同型なコピーを同一視しても理論の論理構造への影響はないとする主張）については、2018年3月、その主張を展開する数学者2名と数理研で（対面で）約一週間に及ぶ議論を行なった際、先方は上記主張を何度も何度も明示的に繰り返し述べており、私だけでなく、私以外の参加者も鮮明に記憶している通り、上記主張はまさしく約一週間に及んだ議論の中心的な話題であった。にも関わらず、 [EssLgc] §3等で詳細に解説しているこのRCSの主張は、主張の当事者を個人的に侮辱することのみを目的とする望月によるでっち上げに過ぎないと主張する第三者たちがネットを賑わせている状況に対して、主張を展開した当事者2名は当該主張をしたことを認めることを拒否している。以下では、この問題を「主張内容の認定問題」と称することにする。

・上記主張内容の認定問題とも深く関係しているが、主張の当事者も、多くの第三者も、主張の当事者が執筆した10㌻程度の有名な原稿の最後の2㌻程度の議論によって宇宙際タイヒミューラー理論に本質的な間違いがあることを証明したと主張しているにも関わらず、その最後の2㌻程度の議論の設定と、元々の宇宙際タイヒミューラー理論の設定の間にどのような論理的関係性があるかについて、詳細な証明どころが、正確な陳述（statement）もどこにも述べられていない（詳しくは、 [Rpt25] §1.3後半をご参照いただきたい）。このような状況によって、この最後の2㌻程度の議論を根拠とする、宇宙際タイヒミューラー理論に対する否定論は、数学的根拠が一切存在しない、ただの「信仰」の域を出ない言説に留まったままの、極めて遺憾な状態が長らく続いている（「信仰」と「権力」の癒着については、詳しくは以前のブログ記事、それから [Rpt25] §3.1 (Fth1), (Fth2)をご参照いただきたい）。

このような言動は、信仰を排して論理的理性を基本とする純粋数学という学問の精神を根底から否定し、純粋数学のみならず、様々な形の文化交流の上に成り立っている国際的な信頼関係を根源的に破壊する性質のものであり、決して宇宙際タイヒミューラー理論という特定の理論やその理論に深く関わっている比較的少数の研究者だけの問題ではありません。

世界各国を見回すと、大量移民と、各国独自の文化・文明の保全を目指す動きの対立に絡む様々な問題・矛盾への対応を背景に、戦後長らく堅持されてきたはずの、法の支配や立証責任等の基本的な民主主義的価値観に基く秩序、それからその秩序を支えた国際的な信頼関係が、欧米を中心に、グラグラと揺らぎ始め、怪しくなりつつある現在、このような状況下において

「一体、誰を、何を、信じたらよいか」

という問い掛けは人類全体の普遍的な課題であり、宇宙際タイヒミューラー理論を巡る状況において、Leanによる形式化のような、論理構造の精密な記述・記録の技術が、新時代の信頼関係の構築の基盤として立派に機能する威力を発揮する事例としてきちんと確立されれば、一学問の一理論の関係者に留まることなく、文明社会全体にとってそれなりに大きな意義や教訓を有する事案になるのではないかという気がしてなりません。

お気に入りの記事を「いいね！」で応援しよう