Looking at the project more I see it's the latter. Turning lean tactics into readable proof text would be hard, as the lean phrase book he is keeping shows: https://docs.google.com/spreadsheets/d/1Gsn5al4hlpNc_xKoXdU6...
Indeed, you can see in the article that the text of Theorem 7.2 omits for brevity details which are present in the non-pretty printed Lean proof (for example H is non-empty, K is a real number, etc.)
My understanding was that the Blueprint tool that he linked is what's responsible for the human-readable math sections shown in the screenshots. I'm not saying it's easy, but it should definitely be doable, basically a spreadsheet like that one on steroids.
I suspect lean will change the thoughts a bit but not eliminate step one. Maybe step three becomes interactive with lean4 etc. and ends in a PR with green build, but the work does not seem likely to end there.
Put it this way: Terrence Tao is unbelievably better at maths than I am; Terrence Tao with lean4 is also unbelievably better at maths than I am with lean4. As far as the value embedded in all already proven mathematics, having it in mathlib is going to make it easy to use, but extending it in the way Prof. Tao can is still pretty hard.
As a side note, I've extended my experimenting with GPT4 from writing Go and emacs lisp to asking it questions about my classes and it does sound smart but will happily give fractional results for an application of Burnside's Lemma, and say things like:
"An example of a simple group without an element of order 2 is any non-abelian simple group of odd order. By the Feit-Thompson theorem, every finite group of odd order is solvable, which means that non-abelian simple groups of odd order do not exist. However, this theorem does not rule out the existence of infinite simple groups of odd order."
Now this answer is correct in describing how (Feit-Thompson theorem) to show that there are no simple groups of odd order, but "infinite simple groups of odd order" is pretty non-sensical. If the order is infinite, it is not odd.
One hopes future iterations will develop understanding in a way that this text lacks.
If I was doing a Math degree right now, that's exactly the kind of stuff I'd want to do for my thesis, kind of jealous tbh.
Once you have produced examples of correct math that way, you can use those to fine-tune the model.
There was this project to use Lean to prove a theorem of Peter Scholze's (Scholze is a well-respected professor and a famous mathemtician). Apparently, it was so big and complex that he could barely keep it in his head, so after writing the proof, he and Kevin Buzzard formalized it with Lean.
https://www.quantamagazine.org/lean-computer-program-confirm...
Then, 6 months later, he was interviewed, where he talks about using Lean for proving his theorem:
https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-...
And the experiment was finished in 2022. Announcement: https://leanprover-community.github.io/blog/posts/lte-final/
Once the language designers had figured out the hardware was now capable enough to make libraries useful, it only took one programmer to do that tedious work. After that all other programmers could reuse that work.
This will be similar: once a large body of definitions and proofs has been built, mathematicians will be able to reuse higher-level constructs to build proofs for their theorems.
It likely also will be similar in that there will be multiple approaches to this with one (or a few; it could be that one system works best/will have the largest set of definitions for one branch of mathematics, while another ‘wins’ in another) ending up victorious.