I got very serious recently about using formal languages in mathematics, and I am trying (like I did once with Magma) to internalize how they function and how I can think in them naturally and basically keep up with a formal proof like I can grasp the flow of regular mathematical text in my field. Obviously, due to the popularity, structure of the type theory, and expressive power (+Mathlib), I decided to explore in depth Lean and one other language which I've built with agents for Peano arithmetic. So far, the main obstacle I can see is that the architecture of many tactics makes it super unfriendly to follow the proof. This is one of those gaps + strange syntax in Lean which still makes me very confused when I try to read such a text. I don't have such problems with Magma, where the ideas are encoded in a much more natural way. This is probably one of those directions in which I want to develop: how to make formal languages which are easy to follow, have a particular deduction style, or are simply expressive enough to make the argument look very compact, yet understandable. In hindsight, I can see that these were some of the problems which Georg Cantor had when he tried to formalize the mathematical work of the day. I had a look at Anthropic's formalization of FLT and... there is so much work :) I can definitely sympathize with Kevin Buzzard that his quest is different. We can appreciate some proof artifact, but the composition of the code, high-level engineering, and difficult choices about how things should be formalized to make them work better (filters for limits...) are equally important, or sometimes even more important than a particular proof artifact itself. Overall, mathematics is an art of exploring new avenues, and Lean and other formalized languages give us so much space for beautiful discoveries, new engineering, and can simply help us organize human knowledge better. So yes, learn formalization as something entirely new, a higher, deeper insight into thoughts. You won't be disappointed, maybe only with how badly AI is still doing this autonomously. We should keep improving this too. Going back to work on elliptic curves in Lean :)