>>317
>ちなLeanによるIUTの証明は遠アーベル幾何学をほぼ全てLeanで実装するであろうことから数万行規模のプロジェクトになる
それで事足りるなら遠アーベル幾何学者なら証明の正誤判断できそう
知らんけど、IUTってそんなレベルじゃないんじゃないかな　言語が未完成だなんだって言われてるようだし　そもそも機械判定を利用できるレベルなんだろうか
あとプロジェクトということはプロジェクト管理が必要になるんだけどあの人たちにそんな芸当できるんだろうか　PMP資格保持者いなさそう