IUT論文AIに読み込ませて、定理3.11から系3.12を導く過程をLEANでやらせてみりゃわかるけど、部品と補題が多すぎるねん
それらの定式化だけで数万行軽く行く
LANAは遠アーベル幾何学のライブラリ実装も兼ねてるって話だから7月17日の中間報告ではGithubが流石に公開されると思うから期待やね
Githubの公開がなかったらそれだけでガッカリや