Since the LANA project apparently isn't releasing theirs, here's my own Lean formalization of IUT.https://github.com/Takkun-kohinata/IUT_LEANbut, commnet is japanese only.use ai agent for translate in your language.