まぁなんでもやってみたらいい。
iutが既存の数学体系に乗るならLeanが保証してくれる。
乗らないならどんな言語体系、推論体系持つのか、望月先生によれば学部生でもできるらしいから、ゲンツェンなりヒルベルトなり横目で見ながらiut基礎論自作してiut版leanでも作って通して見せればいい