Project Lana attempts to formalize hard to understand Mochizuki's IUT in Leananabelian.org 3 pointsur-whale1 month ago1 commentSaveHideCopy link On HNComments−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).