Post #1558699

I found out from Mochizuki's recent talk about AI/formalisation for mathematics, that someone managed to recently convince him about something Zoran Skoda and I knew and understood about the set-theoretic material in IUT4 in late 2012, specifically about what he called 'species' and 'mutations'. But also, the next step is to fully convince him that POV is wholly unnecessary. He mentioned this as well, in light of him looking to use Lean to formalise parts of IUT, but then gently insisted it would be still good to take that approach (viz use a deep embedding of the syntactic category of ZFC in Lean, and work inside that) since the original papers do.