LANA_report_202607

> It would be nice if someone used AI and/or Lean to sort out the abc conjecture, an important unsolved problem in Diophantine analysis. People did attempt this: https://github.com/katobungen/LANA_report_202607/blob/pdf/LA... See also https://www.math.columbia.edu/~woit/wordpress/?p=15770 Here are Kirti Joshi's comments about the LANA project report: https://bpb-us-e2.wpmucdn.com/sites.arizona.edu/dist/4/404/f...

This is a reference to Inter-Universal Teichmüller Theory. Its Wikipedia article gives a good overview (https://en.wikipedia.org/wiki/Inter-universal_Teichm%C3%BCll...). In maths lasting disagreements over a published "proof" are rare, but IUTT is an example of it. What the article misses: There is a more recent, ongoing effort to formalize the published proof in Lean under the name of "LANA" (e.g. see https://zen.ac.jp/news/zmcpostevent0717e and https://github.com/katobungen/LANA_report_202607/blob/pdf/LA... for a recent update). I guess most mathematicians agree that a successful compile of the proof in Lean would confirm its validity. My personal impression is that the process got stuck at the very point Peter Scholze and Jakob Stix pointed out 8 years ago. Officially LANA has still not reached a conclusion.

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).

Here's the report: https://github.com/katobungen/LANA_report_202607/blob/pdf/LA...