ZEN數學中心宣布新專案「LANA」，旨在透過電腦驗證宇宙際Teichmüller理論（IUT理論）
ZEN數學中心與全球三所大學啟動國際合作研究專案「LANA」，旨在形式化遠阿貝爾幾何學並透過電腦驗證IUT理論。
📋 文章處理履歷
- 📰 發表: 2026年3月31日 23:00
- 🔍 收集: 2026年4月1日 13:39（發表後14小時39分鐘）
- 🤖 AI分析完成: 2026年4月17日 01:40（收集後372小時1分鐘）
ZEN大學「ZMC（ZEN Mathematics Center: ZEN數學中心）」於2026年3月31日（週二）宣布了新專案「LANA」。LANA是一個以ZEN大學（日本）、烏特勒支大學（荷蘭）和亞伯達大學（加拿大）為中心的國際合作研究專案，其主要目標是將數論幾何學的重要領域——遠阿貝爾幾何學進行形式化，並驗證京都大學數理解析研究所望月新一教授提出的宇宙際Teichmüller理論（IUT理論）。
本專案（包括準備期）自2023年秋季以來一直在幕後進行活動。3月31日在東京都內舉行的本次發表會上，首次公開了LANA專案的成立經過、目的、基本方針、核心成員、目前的活動狀況以及未來的展望。
**關於LANA專案**
LANA是「Lean for ANAbelian geometry」的縮寫。專案的第一個目標是利用證明輔助系統Lean，將日本研究人員引領世界的數論幾何學重要領域——遠阿貝爾幾何學的主要定理形式化，並建立其函式庫。第二個目標是利用Lean將IUT理論形式化，並進行驗證。
Lean是一種函數式程式語言，它本身並不能自動證明數學定理。通常，要將以日語或英語等自然語言和數學公式描述的數學論證形式化為Lean的語言，需要盡可能地消除歧義並進行改寫。特別是對於像IUT理論這樣龐大而複雜的理論，這項工作不僅僅是機械轉換，而是以對理論本身深刻的專業理解為前提。
LANA專案旨在保持中立的視角，不偏向任何特定立場，將IUT理論整理成可形式化的形式，並進行驗證。在數學家們對該理論的正確性仍存在分歧的情況下，明確論點並以可共享的形式呈現是本專案的重要意義。
**成立經過**
LANA專案構想的背景是近年來數學形式化的巨大進展。特別是，由菲爾茲獎數學家彼得·舒爾策（Peter Scholze）提出的「Liquid Tensor Experiment」是一個標誌性案例，它證明了現代數學的高度複雜論證確實可以利用Lean進行驗證。主導該專案的約翰·科梅林（Johan Commelin）和亞當·托帕茲（Adam Topaz）也是本次LANA專案的核心成員。
鑑於這些先例，ZMC一直在探討透過形式化這種方法，以新的方式面對現代數學重要理論的可能性。作為國際合作研究的LANA專案，正是因此而啟動。
**LANA專案核心成員**
加藤文元（ZEN大學教授・東京科學大學名譽教授，專案負責人）
約翰·科梅林/Johan Commelin（烏特勒支大學助理教授）
基蘭·凱德拉亞/Kiran Kedlaya（加州大學聖地牙哥分校教授）
星裕一郎（京都大學數理解析研究所副教授）
亞當·托帕茲/Adam Topaz（亞伯達大學副教授）
此外，還有約7名年輕成員，包括學生和博士後研究員（來自3個國家/地區）參與，在國際化、多層次的研究體制下推進活動。
**IUT理論驗證的現狀與未來展望**
LANA專案一年多來，在日本、加拿大、荷蘭、美國等地多次舉辦集訓和集中研究會，致力於IUT理論的理解和驗證。結果，研究團隊目前對理論的理解程度以及哪些點仍無法理解，已經變得相當明確。此外，我們正在努力將我們尚未理解的點，盡可能地用淺顯的數學語言來表達。
LANA專案預計於2026年7月17日（週五）舉行活動中期報告記者會。屆時計劃詳細公布IUT理論的驗證結果。
**評論**
**若山正人（ZEN大學校長）**
ZEN大學於去年4月開學，旨在透過建立一所全面的線上大學，緩解和解決我國嚴重的教育差距。我們致力於運用網路和AI等最新的IT技術，創造出傳統大學難以實現的新型大學教育模式。
另一方面，作為一所大學，支持教育基礎並豐富人類智慧財產的研究也是一個重要支柱。本校正在系統性地推進一些傳統大學較少涉足的研究主題。ZEN數學中心在基於電腦計算能力飛躍性進步的尖端數學領域的國際專案「LANA」就是其中之一，並被定位為本校的新挑戰。
**加藤文元（ZEN大學教授／ZMC所長，LANA專案負責人）**
LANA專案是一項國際合作研究，它以證明輔助系統Lean的形式化這一新方法，應對現代數學最前沿的遠阿貝爾幾何學和IUT理論。IUT理論龐大而複雜，其正確性至今仍讓世界各地的數學家們意見分歧。我們匯集了最優秀的團隊，一年多來一直在討論這個理論。結果，我們認為目前對其理解的程度以及哪些點仍無法解釋，已經變得相當明確。然而，我們目前尚未得出結論，這究竟是真正的數學鴻溝，還是我們自身理解的問題。因此，我們打算今後繼續保持中立立場進行探討，並推進與望月教授的對話。在7月17日的中期報告中，我們計劃向全世界公布我們屆時的理解。
**關於發表會的錄影**
3月31日在東京都內舉行的本次發表會的錄影可在以下直播網站觀看。此外，LANA專案核心成員的評論除了發表會錄影外，也可在ZMC網站上查看。
**【發表會錄影】**
* YouTube：https://www.youtube.com/live/b9ZV-4T3iUo
* Nico Nico Live：https://live.nicovideo.jp/watch/lv350105847
**關於ZMC（ZEN Mathematics Center; ZEN數學中心）**
ZMC是一個國際研究機構，旨在推動和發展以數論幾何學為中心的現代數學，以及利用電腦語言進行現代數學形式化（formalization）。
ZMC網站：https://zen.ac.jp/zmc
**關於ZEN大學**
ZEN大學利用尖端IT技術，為所有人提供大學入學機會。ZEN大學唯一的學部「智能資訊社會學部」透過學習不偏向特定學術領域的知識，可以掌握在劇變的AI時代中活躍所需的素養。
2025年10月入學生的申請將於2025年7月23日（週三）開始受理。此外，2026年4月入學生的申請將於2025年9月2日（週二）開始受理。ZEN大學為了廣泛提供高等教育機會給有學習意願的人，入學選拔不進行學力測驗。將依據志願理由和小論文進行選拔。
更多詳細資訊，請參閱ZEN大學網站及簡章。
ZEN大學相關詳細資訊：https://zen.ac.jp/
索取最新簡章：https://zen.ac.jp/form
本專案（包括準備期）自2023年秋季以來一直在幕後進行活動。3月31日在東京都內舉行的本次發表會上，首次公開了LANA專案的成立經過、目的、基本方針、核心成員、目前的活動狀況以及未來的展望。
**關於LANA專案**
LANA是「Lean for ANAbelian geometry」的縮寫。專案的第一個目標是利用證明輔助系統Lean，將日本研究人員引領世界的數論幾何學重要領域——遠阿貝爾幾何學的主要定理形式化，並建立其函式庫。第二個目標是利用Lean將IUT理論形式化，並進行驗證。
Lean是一種函數式程式語言，它本身並不能自動證明數學定理。通常，要將以日語或英語等自然語言和數學公式描述的數學論證形式化為Lean的語言，需要盡可能地消除歧義並進行改寫。特別是對於像IUT理論這樣龐大而複雜的理論，這項工作不僅僅是機械轉換，而是以對理論本身深刻的專業理解為前提。
LANA專案旨在保持中立的視角，不偏向任何特定立場，將IUT理論整理成可形式化的形式，並進行驗證。在數學家們對該理論的正確性仍存在分歧的情況下，明確論點並以可共享的形式呈現是本專案的重要意義。
**成立經過**
LANA專案構想的背景是近年來數學形式化的巨大進展。特別是，由菲爾茲獎數學家彼得·舒爾策（Peter Scholze）提出的「Liquid Tensor Experiment」是一個標誌性案例，它證明了現代數學的高度複雜論證確實可以利用Lean進行驗證。主導該專案的約翰·科梅林（Johan Commelin）和亞當·托帕茲（Adam Topaz）也是本次LANA專案的核心成員。
鑑於這些先例，ZMC一直在探討透過形式化這種方法，以新的方式面對現代數學重要理論的可能性。作為國際合作研究的LANA專案，正是因此而啟動。
**LANA專案核心成員**
加藤文元（ZEN大學教授・東京科學大學名譽教授，專案負責人）
約翰·科梅林/Johan Commelin（烏特勒支大學助理教授）
基蘭·凱德拉亞/Kiran Kedlaya（加州大學聖地牙哥分校教授）
星裕一郎（京都大學數理解析研究所副教授）
亞當·托帕茲/Adam Topaz（亞伯達大學副教授）
此外，還有約7名年輕成員，包括學生和博士後研究員（來自3個國家/地區）參與，在國際化、多層次的研究體制下推進活動。
**IUT理論驗證的現狀與未來展望**
LANA專案一年多來，在日本、加拿大、荷蘭、美國等地多次舉辦集訓和集中研究會，致力於IUT理論的理解和驗證。結果，研究團隊目前對理論的理解程度以及哪些點仍無法理解，已經變得相當明確。此外，我們正在努力將我們尚未理解的點，盡可能地用淺顯的數學語言來表達。
LANA專案預計於2026年7月17日（週五）舉行活動中期報告記者會。屆時計劃詳細公布IUT理論的驗證結果。
**評論**
**若山正人（ZEN大學校長）**
ZEN大學於去年4月開學，旨在透過建立一所全面的線上大學，緩解和解決我國嚴重的教育差距。我們致力於運用網路和AI等最新的IT技術，創造出傳統大學難以實現的新型大學教育模式。
另一方面，作為一所大學，支持教育基礎並豐富人類智慧財產的研究也是一個重要支柱。本校正在系統性地推進一些傳統大學較少涉足的研究主題。ZEN數學中心在基於電腦計算能力飛躍性進步的尖端數學領域的國際專案「LANA」就是其中之一，並被定位為本校的新挑戰。
**加藤文元（ZEN大學教授／ZMC所長，LANA專案負責人）**
LANA專案是一項國際合作研究，它以證明輔助系統Lean的形式化這一新方法，應對現代數學最前沿的遠阿貝爾幾何學和IUT理論。IUT理論龐大而複雜，其正確性至今仍讓世界各地的數學家們意見分歧。我們匯集了最優秀的團隊，一年多來一直在討論這個理論。結果，我們認為目前對其理解的程度以及哪些點仍無法解釋，已經變得相當明確。然而，我們目前尚未得出結論，這究竟是真正的數學鴻溝，還是我們自身理解的問題。因此，我們打算今後繼續保持中立立場進行探討，並推進與望月教授的對話。在7月17日的中期報告中，我們計劃向全世界公布我們屆時的理解。
**關於發表會的錄影**
3月31日在東京都內舉行的本次發表會的錄影可在以下直播網站觀看。此外，LANA專案核心成員的評論除了發表會錄影外，也可在ZMC網站上查看。
**【發表會錄影】**
* YouTube：https://www.youtube.com/live/b9ZV-4T3iUo
* Nico Nico Live：https://live.nicovideo.jp/watch/lv350105847
**關於ZMC（ZEN Mathematics Center; ZEN數學中心）**
ZMC是一個國際研究機構，旨在推動和發展以數論幾何學為中心的現代數學，以及利用電腦語言進行現代數學形式化（formalization）。
ZMC網站：https://zen.ac.jp/zmc
**關於ZEN大學**
ZEN大學利用尖端IT技術，為所有人提供大學入學機會。ZEN大學唯一的學部「智能資訊社會學部」透過學習不偏向特定學術領域的知識，可以掌握在劇變的AI時代中活躍所需的素養。
2025年10月入學生的申請將於2025年7月23日（週三）開始受理。此外，2026年4月入學生的申請將於2025年9月2日（週二）開始受理。ZEN大學為了廣泛提供高等教育機會給有學習意願的人，入學選拔不進行學力測驗。將依據志願理由和小論文進行選拔。
更多詳細資訊，請參閱ZEN大學網站及簡章。
ZEN大學相關詳細資訊：https://zen.ac.jp/
索取最新簡章：https://zen.ac.jp/form
常見問題
LANA專案的主要目標是什麼？
將遠阿貝爾幾何學形式化，並透過電腦驗證望月新一教授的宇宙際Teichmüller理論（IUT理論）。
什麼是IUT理論？
這是京都大學望月新一教授提出的數論幾何學理論，據稱與ABC猜想的證明有關，但其正確性仍在數學界引起爭議。
Lean是什麼樣的工具？
Lean是一種證明輔助系統（函數式程式語言），用於形式化地描述數學定理和證明，並透過電腦驗證其正確性。