A few years ago I asked Mochizuki via email if he would be interested in organising with me an effort to mechanise his proof. At the time I was developing a col

A few years ago I asked Mochizuki via email if he would be interested in organising with me an effort to mechanise his proof. At the time I was developing a collaborative interactive theorem prover, for which this would be an ideal application. He politely declined, and I am kind of happy about this now, because I need a few more years anyway before my theorem prover could be used for something like this without being a pain for its users :-D