3 points | by ur-whale 14 hours ago ago
1 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).
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).