>>642

若山zen大学学長

>本プロジェクトの目的は二つです。

ひとつは日本の研究者の貢献が著しい遠アーベル幾何学の主要定理をLean形式化し、そのライブラリを構築することです。
もう一つは京都大学数理解析研究所の望月新一教授による宇宙際タイヒミュラー理論の、Lean形式化による検証です。