Comment on Project Lana attempts to formalize hard to understand Mochizuki's IUT in LeanComments−ur-whaleOP1moAn 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_202607Mochizuki 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).
Comments
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).