LANA プロジェクト発表にあたって

2026年3月31日に行われたLANAプロジェクト発表に際しての各員のコメントを掲載いたします。

若山正人：ZEN 大学学長

学長の若山です。

本日はお忙しいなか、本学ZEN数学センター（ZMC）の「LANAプロジェクト」発表の場にお越しいただき感謝申し上げます。AI時代に入った現在、純粋数学においても本質的な場面でのコンピュータ証明の有効性や可能性の広がりが現実味を帯びています。今日は、このZMCのプロジェクトについて、ご報告申し上げたく存じます。プロジェクト名は証明支援系Leanと数論幾何学の一分野である遠アーベル幾何学に基づくものですが、詳細については、後ほどZMC所長であり本プロジェクトの推進を担う加藤文元教授が行います。私からは、なぜ、本日の発表となったかについてご説明したく思います。

本学は、本格的なオンライン大学をつくることで日本の深刻な教育格差の緩和・解消を図るために昨年4月に開学しました。インターネットやAIなどの最新のIT技術を駆使することにより、既存の大学では実現が難しかった新しい大学教育の形を作り上げることを目指しています。一方で、大学である限り、教育を底から支え、人類の知的財産を豊かにする学問研究もまた大きな柱です。ZEN大学では、既存の大学ではあまり取り組んでいなかったいくつかのテーマに関する研究を組織的に進めており、その一つが今日ご紹介するZMCによるLANAプロジェクトです。

数学において、以前はLeanを使った研究は盛んではありませんでした。しかし、コンピュータの計算能力の飛躍的向上とAIによる自動証明の可能性が窺えるようになり、今や脚光を浴びているものです。Leanは、汎用プログラミング言語でありながら定理証明支援系でもあるという特徴を持ちますが、それ自体はAIに無関係です。AIとともに語られることもあるのは、人間が使う自然言語と数式をコンピュータ言語に翻訳する、つまり形式化の際に、AIによる自動形式化の機会があるからです。歴史的に長く研究され、理論体系が整った分野には、膨大な研究成果と方法論の蓄積があるため、一部ではこの自動形式化も期待されています。

海外に目を向けると、現代数学の問題をLean形式化によって発展させようという試みが、たとえば、フィールズ賞受賞者でもあるTerence Taoらが中心となって進んでいます。また最近、私自身もシンガポール国立大学の数理科学研究所での「AIと数学」というテーマの会議の一部に出席し、Kazhdan-Lusztig予想やaffine Deligne-Lusztig 多様体といった、表現論・整数論分野におけるLean形式化による興味深いチーム研究の成果に触れて参りました。数学研究の大きな潮流になると考えています。おそらくわが国においても Leanを用いた研究が各所で試みられていると思います。しかし組織立って本格的に、という姿は見えていません。こうした状況もあり、LANAプロジェクトの推進を決めました。

本プロジェクトの目的は二つです。ひとつは日本の研究者の貢献が著しい遠アーベル幾何学の主要定理をLean形式化し、そのライブラリを構築することです。もう一つは京都大学数理解析研究所の望月新一教授による宇宙際タイヒミュラー理論の、Lean形式化による検証です。この理論については、未だ世界の数学者からの納得感が得られないままの状況です。したがってその検証自体が、数学の発展にとって意義深いはずです。今回、加藤教授が中心となり、目的達成のために世界に比類ない国際チームを整えることができました。限られたテーマ・分野ではありますが、考えうる世界最高チームです。

これは本学の新しい挑戦です。本日はどうぞよろしくお願い致します。

加藤文元：ZMC 所長

本日はお集まりいただき、誠にありがとうございます。

本日の記者発表では、私たちが新たに「LANAプロジェクト」を開始したことを、皆様に正式にご報告申し上げます。このLANAプロジェクトについては、今日まで、その存在も含めて一切公開してきませんでした。しかし、実はこのプロジェクトは、その準備期間も入れると、すでに2023年秋から始まっております。プロジェクトが本格的に始動したのは2024年9月ですので、すでに1年半以上にわたって活動を続けていることになります。

まず最初に、LANA、すなわち「Lean for ANAbelian geometry」というプロジェクトの目的についてお話し致します。このプロジェクトの目的は大きく分けて2つございます。

第1の目的は、遠アーベル幾何学の形式化とそのライブラリ構築です。「遠アーベル幾何学」というのは、従来より日本人の研究者が顕著に活躍している、数論幾何学の重要分野です。LANAプロジェクトでは、この遠アーベル幾何学の主要定理とその証明を計算機上の証明支援系Leanを用いて形式化し、そのライブラリ構築を目指します。それと同時に、日本の数学界におけるLeanの普及と、コミュニティ形成をうながすため、研究集会などさまざまなイベントを企画して参ります。

第2の目的は、京都大学数理解析研究所の望月新一教授による宇宙際タイヒミュラー理論、いわゆるIUT理論を、同じくLeanの形式化によって検証することです。私たちは、特定の立場に偏ることなく、中立的な視点から、この理論を形式化可能な形に整え、その検証を行うことで、同理論に関する長年にわたる論争に終止符を打つことを目指しています。

これらの目標を達成するため、本プロジェクトでは世界中から強力なメンバーを集めました。私としては、このメンバーはこれらの目標を達成する上で、まさに世界一のメンバーである、と自負しております。

では次に、LANAプロジェクトのコアメンバーをご紹介致します。コアメンバーは5名おります。Utrecht大学のJohan Commelin、カリフォルニア大学サン・ディエゴ校のKiran Kedlaya、京都大学数理解析研究所の星裕一郎、Alberta大学のAdam Topaz、そして私、プロジェクトリーダーの加藤文元です。これらのコアメンバーのほかに、学生やポスドクなどの若手メンバーが7名ほど参加しています。今回、Commelin, Kedlaya, Topazの三氏は、オンラインでこの発表会に参加しておりますので、後ほどスピーチを致します。星裕一郎は所用のため欠席しておりますが、メッセージをもらっておりますので、後ほど私が代読いたします。

このメンバーの実績について、ひとつお話ししておきたい点がございます。2020年12月に、フィールズ賞数学者Peter Scholze氏　—　この人はIUT理論に対して否定的な見解を公にしていることでも有名ですが　—　（このScholze氏）のチャレンジから始まったLiquid Tensor Experimentという、現代数学の形式化プロジェクトがありましたが、これが2022年7月、Scholze氏の挑戦からわずか1年半で、Leanによって完成しました。この出来事はLeanによる形式化の威力を、世界中に示すきっかけともなりました。実はこのLiquid Tensor Experimentを完成させたのは、ほかでもない当プロジェクトのJohan CommelinとAdam Topazがリーダーとして主導したチームです。実は私はこの出来事に強い衝撃を受け、LANAプロジェクトを構想するに至りました。

ここで、Leanによる数学の形式化について、ごく簡単に説明致します。Leanとは、いわゆる証明支援系と呼ばれている関数型プログラミング言語のひとつです。「証明支援系」という言葉を聞くと、あたかもそれ自体が人間に代わって数学の定理を証明してくれるようなものを想像するかもしれませんが、実はそういうものではありません。ふつう数学の議論は、日本語や英語などの自然言語と数式とを併用しながら記述されます。これに対して、Leanなどの証明支援系による形式化とは、そのような数学の議論を、プログラミング言語に書き換えることです。言い換えれば、自然言語から形式言語への翻訳です。それを行うには、自然言語がもつ曖昧さをできるだけ排除し、省略されている行間を埋めていかなければなりません。したがって、形式化とは、数学の議論の筋道を、より厳密で、より共有しやすい形に整える作業であると言えます。

しかしながら、IUT理論は巨大で複雑な理論であり、しかもその正否については現在でも世界の数学者たちの意見は分かれています。したがって、その形式化の作業は、単なる機械的な翻訳　—　そのようなものが可能だと仮定しての話ですが　—　（単なる機械的な翻訳）では済まされません。作業を進める私たち自身が、IUT理論について十分に深い理解に達してしていなければなりません。そのためLANAプロジェクトでは、1年以上にわたってIUT理論について集中的に議論を重ねてきました。日本、カナダ、オランダ、アメリカなど各地で合宿を行い、論文など各種の資料を読み、論点を整理し、互いの理解を突き合わせながら、検証のための土台を築いてきました。

その結果として、現在我々はIUT理論に関して、かなり深い理解をメンバーの間で共有できるようになったと自負しております。それによって、私たちはどこまでちゃんと理解できていて、どこがどのように解明できていないのか、明瞭に言い表せるようになってきました。そして重要なのは、そのいまだ解明できていないポイントを、平易な数学の言葉で表現できるようになった、ということです。

ここで慎重に申し上げるべきは、現時点でそのポイントが数学的なギャップであるのか、それとも私たち自身の理解力の問題に由来するのかについて、私たちはまだ最終的な結論を出していない、ということです。数学とは客観的な学問ですが、その客観性に忠実な言い方をするとして、あくまでも可能性としては、この点に議論の不備があるという可能性はもちろんあります。ですから、まさにこの点こそが今後の核心的論点であり、私たちは今後もこの点について、あくまでも中立的な立場から検討を進め、望月氏との対話も続けていくつもりです。

今後の見通しについて申し上げます。私たちは、今年の7月17日に、LANAプロジェクトの活動に関する中間報告を、記者会見の形で世界に向けて発表する予定です。その場では、IUT理論の検証について、その時点までの我々の理解の詳細を整理して公表したいと考えています。そこには、私たちが理解できた点だけでなく、まだ理解ができていない点、そしてそれをどのように言語化し、どのように位置づけているかということも含まれます。言い換えれば、私たちは7月17日の記者会見までに、これらの論点と、その時点での検証結果を中間報告としてまとめ、世界に提示するつもりです。

私たちは、数学の深い理解と計算機による厳密な確認とを並行して追求することによって、新しい数学研究の地平を切り開くことができると信じています。LANAプロジェクトは、そのための挑戦です。引き続き誠実に、粘り強く、この課題に向き合って参りたいと思っております。

引き続きまして、この後は、オンライン参加者たちにスピーチしてもらいます。まず最初に、Johan Commelinが、将来の数学研究におけるLean形式化の意義や、日本におけるコミュニティ形成の必要性などについてお話し致します。続いてAdam Topazからは、数学研究のやり方がLeanによって大きく変わる可能性があること、そしてIUT理論をめぐる我々の研究の現状と展望についてコメントしてもらいます。Kiran Kedlayaからは、彼自身のIUT理論との関わりや、コンピューターによる数学の形式化が将来の数学にもたらすインパクトについて話してもらいます。

それではここで、私の話しは終わりとさせて頂きます。ご清聴ありがとうございました。

Johan Commelin（Utrecht）

皆様、本日これまでの発表に、私から一言付け加える機会をいただき、心より感謝申し上げます。

加藤教授からお話がありました通り、アダム・トパーズ氏と私は「Liquid Tensor Experiment」を主導して参りました。このプロジェクトが成功裏に完了した後、多くの人たちから「Leanを用いてIUT理論を検証すべきではないか」という問いを投げかけられました。

その際の私の答えは一貫して、「日本の数学コミュニティの人たち、すなわちIUT理論の専門知識を持つ人たちが関与してくれる場合に限る」というものでした。ですから、加藤教授からLANAプロジェクト立ち上げの提案をもらったときの私の興奮は、皆様にも想像していただけるかと思います。

本プロジェクトにおいて、私が強調したい点は3つございます。

第一に、ZEN数学センター（ZMC）と共に、日本の数学界において「形式化」および「Lean」のコミュニティを構築できることを、大変喜ばしく思っております。私は、数学とは「インフォーマルな直観」と「フォーマルな厳密性」との間の対話であると信じています。数学のLean化・機械化は、この対話においてますます重要な役割を果たしつつあります。合宿や研究集会を通じて、この取り組みを牽引していく一員となれることを誇りに思います。

第二に、LANAプロジェクトの一環として、私たちは遠アーベル幾何学の基礎をLean上に構築しています。一例を挙げれば、ガロア圏や基本群の理論などです。現在、代数幾何、数論幾何、そして遠アーベル幾何学の基盤となる部分が、Leanの共有ライブラリである「Mathlib」へと着実に提供されています。これは、将来的に他の形式数学プロジェクトを積み上げていくための、堅固な土台となるものです。

そして最後に、Leanを用いることで、私たちはIUT理論における主張や議論を、極めて正確かつ厳密なものにすることができます。ここで、本プロジェクトにおいて「形式的な検証（Formal Verification）」と「生成AIによる予測」を明確に区別しておくことが不可欠です。生成AIは統計的なパターンに基づいてテキストを合成するため、いわゆる「ハルシネーション（もっともらしい嘘）」を引き起こす可能性があります。これに対し、Leanは厳格な論理規則に照らして数学的真理を検証します。これにより、数学のインフォーマルな提示においてしばしば生じる「曖昧さ」を排除することが可能となります。Leanによって検証された証明は、従来の査読プロセスでは到底到達し得ないレベルでの「正しさの保証」を与えるのです。

LANAプロジェクト、ひいては数学界全体におけるこれらの新たな進展に、私は深く胸を躍らせています。この重要なプロジェクトを支援してくださっている川上様、ならびにZEN数学センターに感謝申し上げるとともに、今後の継続的な協力関係を楽しみにしております。

Adam Topaz（Alberta）

私は数学者の中でも、少し特殊な立場にあります。私の研究は、本プロジェクトの両側面—すなわち「遠アーベル幾何学」と、Leanを用いた「形式検証」—の両方にまたがっているからです。この双方に真摯に取り組んできた者として、形式化がいかに数学的思考のあり方を変容させるかを、身をもって経験してきました。これこそが、本プロジェクトが存在する意義の核心であると私は信じています。

数学は何千年も同じ手法で行われてきました。私たちは議論を自然言語で記述し、同僚と共有し、それが正しいかどうかを判断してきました。しかし、形式化は私たちにそれ以上のことを求めます。完全な明示性と正確性を強いるだけでなく、私たちが用いる数学的概念を根本から再考し、最適化することも求めてくるのです。形式化のプロセスには、依然として人間の努力と創造性が不可欠です。証明支援系が担うのは、論理的整合性のチェックです。定義や主張が正しく形式化されているかどうかを判断できるのは、依然として人間の数学者だけなのです。

ある数学理論が十分に巨大で、かつ激しい論争の対象となっている場合、従来の非形式的な検証プロセスは限界を迎えることがあります。誠実かつ注意深く理論を読み込んだ理知的な数学者たちの間であっても、極めて異なる結論に達することがあるのです。形式化は、こうした議論の焦点を曖昧さなく検討するための枠組みを提供します。

まさにその精神で、私たちはIUT理論に向き合ってきました。過去1年半、私たちのチームは形式化を常に念頭に置きつつ、IUT理論に対する深く共有された理解を構築するために多大な努力を注いできました。本プロジェクトを通じて、私たちは幾度となく、理論上の特定の地点に突き当たりました。その都度、私たちは複数の方向からアプローチし、理解を深めてきました。現在、私たちはその地点をLeanで形式化できるほど正確に言語化できる段階には達していますが、そこから先へ進むことができずにいます。これが証明上の真の欠落（ギャップ）を反映しているのか、それとも現在の私たちのIUT理論に対する理解の限界に過ぎないのか、現時点では断定を下すに至っていません。

加藤教授が述べたことを改めて強調したいと思います。私たちは今後もこの点についての検討を続け、望月教授との対話を継続する所存です。私たちは、Leanが提供する正確性が、これまでになく生産的で透明性の高い対話を可能にすると確信しています。数学コミュニティには、この問題について曖昧さのない明晰な結論を得る権利があり、私たちは誠実さと厳密さをもって、その追求にコミットし続けます。

最後に、川上様、加藤教授、そしてZEN数学センター（ZMC）が、これほど真剣な目的を持ってこのチームを結成し、支援してくださったことに深く感謝申し上げます。このプロジェクトの一員であることを誇りに思い、私たちの進捗を世界と共有できる日を楽しみにしております。

ありがとうございました。

Kiran Kedlaya（USCD）

私は数学の形式化に関しては新参者ですが、IUT理論への関心はLANAプロジェクトの前からの長い歴史があります。2015年、オックスフォード大学で開催されたワークショップにおいて、IUT理論に馴染みのなかった多くの数論幾何学者が、望月教授による初期の論文の読解・発表を通じ、この主題を消化しようと一致団結したことがありました。そのワークショップでは、IUT理論に対するコミュニティの理解における突破口を開くには至りませんでしたが、多くの啓示を得る結果となりました。

残念ながら、その後のコミュニティによるIUT理論への取り組みは、進展の遅さに加え、2018年のショルツェとスティックス（Scholze–Stix）の文書によってIUT理論の論理的な根幹に矛盾が指摘されたという見解が広く行き渡ったことにより、停滞してしまいました。当時、私もIUT理論の研究は限定的にしか行っていませんでしたが、一部の専門家との連絡は保ち、関連する会議にもいくつか参加する中で、その「矛盾」の指摘はコミュニケーションの齟齬に起因するものだと確認しました。そのため、IUT理論の状況は依然として未解決のままであると判断していました。

私がLANAプロジェクトに参加したのは、形式化という革命に追いつくためであると同時に、IUT理論およびABC予想の現状について、コミュニティの合意形成を支援するためです。もし本プロジェクトがIUT理論について肯定的な結論に達した場合、私は自身の社会的信用を投じて、その結論を数論幾何学の主流の研究者たちへと伝えていく覚悟でいます。

私が初期の段階で学んだことの一つは、アダム（・トパーズ氏）が指摘した「形式化とは単なるソフトウェアの問題を超越したものである」という点です。これは社会学的な問題でもあります。つまり、正しい数学を構築するために新しいツールを使うためには、私たちは「数学者が正しさについていかにして合意に至るか」というプロセスも考慮しなければならないのです。影響力のある定理の証明が複雑化するにつれ、検証は数学者間の壊れやすい信頼のネットワークに依存するようになりました。人工知能は複雑性を制御する上で大きな可能性を秘めていますが、大規模言語モデルが持つ信頼性の欠如は、その繊細な信頼関係を損なうリスクを孕んでいます。LANAプロジェクトは、洗練されたソフトウェアツールの助けを借りつつ、あくまで「人間の理解」を促進することに主眼を置くという、前進のための道筋を体現しています。今後数ヵ月にわたるプロジェクトチームの継続的な活動を楽しみにしております。また、この研究を可能にしてくださった加藤教授とZEN数学センターに感謝いたします。

星裕一郎：京都大学数理解析研究所

私は、LANAプロジェクトのコアメンバーの一人として、2024年からこのプロジェクトに参加して、メンバーの皆さんと一緒に活動してまいりました。振り返りますと、この1年以上の歩みは、IUT理論をどのように説明するかという問いに正面から向き合い続ける時間であったと感じています。

その中で、私自身が担ってきた役割は、LANAプロジェクトのメンバーに対して、IUT理論の中身をできるだけ網羅的に説明することでした。特に重要なポイントについては、できるだけ丁寧に時間をかけて説明し、単なる概略理解にとどまらず論理の細部まで共有できるよう努めてきました。特に、2021年に出版されたIUT理論の第3論文に書かれている定理3.11から系3.12を導く論理に対する共通理解、それをメンバー内でしっかりと構築することをひとつの大きな目標として、これまで取り組んできました。

そのために、長い時間をかけて議論を重ね、説明を繰り返し、できるだけ多くの角度から論点を整理してきました。その結果として、この1年以上の努力を通じて、メンバーのIUT理論に対する理解は、確実に大きく前進したと確信しています。少なくとも、IUT理論の直接の関係者以外で、これほど真剣にその理解を試みて、そして、これほど粘り強く取り組んだ人たちはそれほど多くない、私はそのように思います。その意味で、このプロジェクトには大きな意義があると感じていますし、また、そのようなプロジェクトに参加していることを、私はとてもうれしく思います。

しかし同時に、残念ながら、私はまだ自分の役割を完全には果たせていないとも考えています。特に、先に述べた定理3.11から系3.12を導く論理について、LANAプロジェクトのメンバーの多くが、その中に何か超えられない壁があると感じていること、その事実を私は重く受け止めなければいけません。そして、そのような状況に対して、自分自身の至らなさも強く感じています。

それでも私は、この1年以上の積み重ねが無意味だったとはまったく思いません。むしろ、ここまで真剣に考え、議論し、理解しようとしてきたからこそ、どこにその本当の難しさがあるのかが、以前よりもはるかに明確になったのだと思います。そのような意味においても、このプロジェクトで積み重ねてきた営みには、確かな価値と意義があると考えています。

最後に、ZEN数学センターおよび加藤文元教授に対して、深く感謝を申し上げます。これまでの様々な多大な支援と尽力なくしては、この有意義な活動は決してあり得なかった、そのことは疑いようのない事実です。本当にありがとうございます。

今後も、残された課題に対して誠実に向き合いながら、メンバーの理解を少しでも前に進める努力を続けていきたいと思います。ありがとうございました。