学部の数学をLeanのライブラリにするのさえ一大プロジェクトなので、その先はまだ夢だな