> there are already (pre AI) machine-generated proofs that we've pretty much agreed not to try to explain fully, like the four-color theorem

Algorithmic verification is a very unsatisfying answer to the problem (e.g., surely it's not just dumb luck that every single case happen to have this exact property), but that's an entirely different issue than saying that no one follows logic of the proof method itself.