・『機械的に検証可能な形に変換』は、証明した本人でなくとも、だれでも出来るのが本当だろう
・しかし、問題はマンパワーと予算で、そういう予算をだれか取って、実行すればいいだろう
・実際、まだまだ『機械的に検証』された定理は数少ない
・もっとも、ChatGpt30くらいのレベルになれば、AI検証できるかも
（結構早くそういう時代が来るかもね）