[cxseven]

For the Kepler Conjecture, human mathematicians first found a way to show that it could be proved by checking a finite (but long) list of computer-verifiable claims.

Here Scholze is saying that part of the proof simply hasn't been written, so there's nothing to verify. I think he's missing that computer verification proponents are also aware of that and are either

1. trying to motivate the camp that claims to understand Mochizuki's work to formalize and computer-verify it

and/or

2. suggesting that some of the gaps can be filled in by automatic theorem provers

[cycrutchfield]

It took like a decade to produce a computer verified proof for the Kepler Conjecture. And that was just for a relatively well-defined exhaustive search. That sounds like a molehill compared to Mochizuki’s Everest of a proof.

[pas]

Methods have improved a lot since then.

The problem is that these papers are vague. The translation to computerized version would be a very different thing, it'd require a lot of creative writing on behalf of the translator.