Putting my neck out here to predict that if he does somehow prove the abc conjecture in a verified theorem prover (that the community acknowledges has the right theorem statement)o that it won’t basically follow the lines of his current claimed proof.
That is, I think his proof is wrong. Furthermore his childish abrasiveness (as I saw in a white paper he put up somewhere) makes me severely doubt his epistemics.
These remarks by LANA core team member Yuichiro Hoshi seem relevant:
I have joined the LANA Project in 2024 as one of the core members and have been working with the other members ever since. Looking back, I feel that this more than a year in the project was a period in which I have continuously confronted the question of how to explain inter-universal Teichmuller theory should be explained.
The role that I myself have undertaken in the LANA project has been to explain the content of inter-universal Teichmuller theory to the members of the project as comprehensively as possible. On particularly important points, I have tried to give explanations as carefully as possible and with as much time as necessary, so that we could share not merely an outline-level understanding but also the details of the logic. In particular, one major goal toward which I have been working has been to establish a understanding, among the members of the project, of the logic by which Corollary 3.12 is derived from Theorem 3.11 of the third paper of the inter-universal Teichmuller theory published in 2021.
To that end, we have spent a great deal of time holding discussions, repeating explanations, and organizing the issues from as many angles as possible. As a result, through these efforts over the past year and more, I am confident that the members’ understanding of inter-universal Teichmuller theory has certainly advanced greatly. At the very least, I do not think that there are many people outside of those directly involved with inter-universal Teichmuller theory who have tried to understand it this seriously and worked on it this persistently. In that sense, I feel that this project is of great significance, and, moreover, I am very happy to be participating in such a project.
At the same time, however, I also believe, regrettably, that I have not yet fully fulfilled my role. In particular, with regard to the logic by which Corollary 3.12 is derived from Theorem 3.11 as I mentioned earlier, I must take seriously the fact that many members of the LANA Project still feel that there is some insurmountable wall there. Then I also keenly feel my own shortcomings in the face of such a situation.
Nevertheless, I do not think at all that the efforts we have made over the past year and more have been meaningless. On the contrary, I think that precisely because we have thought so seriously, discussed so extensively, and tried so hard to understand matters up to this point, it has become far clearer than before where the true difficulty really lies. In that sense as well, I believe that the efforts we have made on this project have definite value and significance.
How corollary 3.12 follows from theorem 3.11 is where everyone outside of Mochizuki’s circle gets stuck (except Kirti Joshi I suppose, who Mochizuki completely dis-endorses). The LANA project (“Lean for ANAbelian geometry”) is what Mochizuki’s note above is about.
Putting my neck out here to predict that if he does somehow prove the abc conjecture in a verified theorem prover (that the community acknowledges has the right theorem statement)o that it won’t basically follow the lines of his current claimed proof.
That is, I think his proof is wrong. Furthermore his childish abrasiveness (as I saw in a white paper he put up somewhere) makes me severely doubt his epistemics.
These remarks by LANA core team member Yuichiro Hoshi seem relevant:
How corollary 3.12 follows from theorem 3.11 is where everyone outside of Mochizuki’s circle gets stuck (except Kirti Joshi I suppose, who Mochizuki completely dis-endorses). The LANA project (“Lean for ANAbelian geometry”) is what Mochizuki’s note above is about.