ZEN大学、IUT理論のPC検証を目指すZMCの新プロジェクト「LANA」を発表

日本財団ドワンゴ学園が設置するZEN大学の「ZEN Mathematics Center（ZEN数学センター、ZMC）」は3月31日、新プロジェクト「LANA」を発表した。

ZEN大学、ユトレヒト大学、アルバータ大学を中心とする国際共同研究として進めるもので、数論幾何学の重要分野である遠アーベル幾何学の形式化と、望月新一・京都大学数理解析研究所教授による宇宙際タイヒミュラー理論（IUT理論）の検証を主な目的に掲げる。

LANAは「Lean for ANAbelian geometry」の略称。証明支援系Leanを用いて遠アーベル幾何学の主要定理を形式化し、関連ライブラリを構築することに加え、IUT理論そのものを形式化し、その検証に取り組む。自然言語と数式で書かれた高度な数学理論をLeanの記述に落とし込むには、曖昧さを極力排した形への書き換えが必要で、とくに巨大で複雑なIUT理論では、単なる機械的変換ではなく深い専門的理解が求められるという。

プロジェクトは2023年秋から準備を含めて活動してきた。背景には、フィールズ賞受賞者ペーター・ショルツェ氏の提起を契機に進んだ「Liquid Tensor Experiment」など、現代数学の形式化が近年大きく進展してきた流れがある。LANAの中心メンバーには、加藤文元・ZEN大学教授をはじめ、ヨハン・コメリン氏、キラン・ケドラヤ氏、星裕一郎氏、アダム・トパーズ氏らが名を連ね、学生や博士研究員を含む若手研究者も加わる国際的な研究体制を構築している。

ZMCによると、これまで1年以上にわたり、日本、カナダ、オランダ、アメリカなどで合宿や研究会を重ね、IUT理論のどこまで理解が進み、どこがなお不明確なのかを整理してきた。現時点では、理解が及ばないポイントをできるだけ平易な数学の言葉で示す作業も進んでいるという。7月17日には中間報告の記者発表を予定しており、その時点での検証結果を詳しく公表する計画だ。

ZEN大学は、このLANAを、コンピューターの計算能力の飛躍的向上を背景に、最先端数学へ新しい方法で挑む研究プロジェクトと位置づけている。