Project Lana attempts to formalize hard to understand Mochizuki's IUT in Lean (anabelian.org) 3 points by ur-whale 1mo ago ↗ HN
[–] ur-whale 1mo ago ↗ 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_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).
1 comment
[ 5.8 ms ] story [ 108 ms ] threadAdditional 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).