I think TFA’s point is that it’s interesting - it’s just not feasible to do what follows after “it’s interesting”, which is to try to make heads or tails of the stack of writing that we’ve been given. Engaging with a well-written proof of a similar scope is enough of a task already.

Isn't it obvious that the feasible way to respond is to start developing AIs that rewrite proofs for human understanding