Maybe IUT would face issues in Lean. But Joshi shouldn’t, so formalizing Joshi can be a warm-up for formalizing Mochizuki, and then if IUT truly can’t be formalized in Lean, we’ve learned something.
I think there’s also interest in understanding IUT independently of the abc conjecture. It’s meant to be a whole new “theory” (in the sense of e.g. Galois theory, a body of original concepts pertaining to a particular corner of math), so someone should be interested in understanding how it works. But maybe you have to be an arithmetic geometer to have a chance of doing that.
What are the formalization disputes you know from elsewhere?
Maybe IUT would face issues in Lean. But Joshi shouldn’t, so formalizing Joshi can be a warm-up for formalizing Mochizuki, and then if IUT truly can’t be formalized in Lean, we’ve learned something.
There is, incidentally, a $1M prize for any refutation of Mochizuki’s proof, to be awarded at the discretion of tech & entertainment tycoon Nobuo Kawakami.
I think there’s also interest in understanding IUT independently of the abc conjecture. It’s meant to be a whole new “theory” (in the sense of e.g. Galois theory, a body of original concepts pertaining to a particular corner of math), so someone should be interested in understanding how it works. But maybe you have to be an arithmetic geometer to have a chance of doing that.
What are the formalization disputes you know from elsewhere?