It’s funny because over the years, when the abc affair was discussed on Internet forums, there would always be commenters who’d say, can’t we resolve Scholze vs Mochizuki by just translating it all into Lean? And then mathematical sophisticates would say, that’s not viable, the disagreement is about subtle concepts that are not easily formalized… But now Mochizuki himself has embraced this plan.
It’s funny because over the years, when the abc affair was discussed on Internet forums, there would always be commenters who’d say, can’t we resolve Scholze vs Mochizuki by just translating it all into Lean? And then mathematical sophisticates would say, that’s not viable, the disagreement is about subtle concepts that are not easily formalized… But now Mochizuki himself has embraced this plan.