the way to interpret the gigantic lean proof is not by inlining each lemma, looking at all the lines, and thinking "yeah that's a lot". That's also not the way to read a paper.
Instead, you proceed in layers of abstraction. For example
1. the main claim may rest on some set of sub-claims, as well as some local (to teh main claim) work to "patch things together"
2. each of those sub-claims themselves may require other sub-claims + local work, etc
These can be collected into a dependency graph. In lean, this is often called a "blueprint". Here is the blueprint for the formalization of the Polynomial Frieman-Rusza conjecture (now a theorem, by Gowers, Green, Manners, and Tao).
https://teorth.github.io/pfr/blueprint/
This layer of abstractions is (roughly) equivalent a different way to format mathematics. You could remove the Lean component (let alone any AI), and create such a dependency graph for a paper. I would argue this is a clearer way to format mathematics (again, ignoring both the formal verification applications of it, as well as AI).
Any mathematics paper intrinsically has a graph such as this underlying it, and tries to make the various linkages in the graph clear via prose. Prose is only so powerful a way to organize things. I'm sure you're familiar with the way early mathematicians would describe various formula (e.g. the quadratic formula) via prose. It is very hard to understand.
Separately from this dependency-graph perspective, you can do things like
1. add formal verification. Now, each component in the dependency graph is verifiable with high confidence (though harder to write and read). This has some benefits and downsides. Harder to write and read is bad. Being able to have high confidence in the veracity of the result is *very* good. It allows larger collaborations in mathematics. Previously, a large collaboration would require all mathematicians to trust eachother to a large extent. This is (practically) difficult.
2. when each component can now be verified to high accuracy, you can now throw AI at it. I won't extoll the virtue of this. There are parts of it that seem interesting, but many "AI for Math" things currently are stil producing unformalized papers (in prose).
Maybe the main thing I'd say is that this type of "graph structure, with each component trusted" is already implicitly what mathematicians do. You write papers that cite other papers etc. Except now, instead of needing to look for status signals to trust papers (or invest personal effort), you can look for another (honestly fairer) signal to trust papers. So there's a sense in which formalization allows for the democratization of mathematics. I do think there's something beautiful about that.