By the way, leaving aside history and motivation and dictionaries, I believe the two most essential papers logically preceding the IUTeich series to be actually, by and large:
- Topics in Absolute Anabelian Geometry III: Global Reconstruction Algorithms (Feb 2012);
and
- The Etale Theta Function and its Frobenioid-theoretic Manifestations (2008).
These are the two most prominent previous papers from each of the two main trends in Mochizuki’s proof: respectively, the “anabelian reconstruction” software [for number fields equipped with a hyperbolic curve related to a once-punctured elliptic curve]; and the “theta-evaluation on l-torsion points” in the spirit of HAT (developed, however, right from the beginning in the rather different framework of “geometry of categories”). They are certainly the two most heavily cited papers in IUTeich.
As for HAT and GTKS proper, it appears that as far as the actual proof is concerned, their results could be best read as guiding principles or heuristics. (While of course they are perfectly rigorous mathematics, and autonomous in their own right ? only insufficient or ill-adapted for the actual diophantine applications.)