Mochizuki's claimed proof of the ABC conjecture is not unintelligable; it has errors. There are no proofs written by humans that are not human-readable, because in order to come out of a human mind, the proof must have fit there originally.
The four color theorem states that no more than four colors are required to color the regions of any map so that no two adjacent regions have the same color. It was the first theorem proved with substantial computer assistance. The theorem was proved by showing there could not be a counterexample. The authors made a list of maps where if a minimal counterexample existed, it would be one of these maps. There were 1,834 maps in that list, and each one was checked by computer. You could turn each of those cases into a picture or paragraph, but the resulting artefact would not meet my definition of human-readable.
Human-readable does not just mean in English. Humans can only hold a few objects in their short-term memory at once, not hundreds. Though some proofs require significant background knowlege, any proof written by a human will respect the fundemental limits of the human mind. There are no proofs written by humans that are not human-readable, because in order to come out of a human mind, the proof must have fit there originally.
I suspect large lean proofs generated by LLMs do not respect the fundemental limits of the human mind. If no human can read and understand them, no one can extract value in the form of reusable techniques, additional problems, progress towards related problems, and everything else Tao mentioned. If LLM proof generators can be made to write proofs with the same value as humans, that would be great! OpenAI would be a celebrated collaborator if they created as much value as a human does.