Leanは数学の証明支援機能を持つ純粋関数型言語でプログラミング言語・システム。
一方、IUTの原理は万物の原理「緩み=不定性」で、数学の証明がない量子力学の不確定性原理まで含み数学の範囲を超えていてる。

つまり望月新一教授のトンデモIUTはLeanの範囲外。