Project Lana attempts to formalize hard to understand Mochizuki's IUT in Lean

An attempt at formalizing in Lean Mochizuki's ITU and put an end to the controversy produced by a 500 pages "proof" that no one can actually understands.

Additional information:

https://github.com/katobungen/LANA_report_202607

Mochizuki himself has also started a "skeleton" formalization attempt of his theory:

https://aitpm.github.io/slides/Mochizuki.pdf?utm_source=chat...

Surprisingly enough, no one seem to have tried to use LLM's to do the work (or parts of it).