I'm going to try formalizing this course in Lean--not sure how hard it is going to be. If anyone is interested in doing the same, please feel free to contribute!
https://www.linkedin.com/posts/lean-fro_leanlang-cslib-forma...
If you don't know, writing a proof in isolation can be difficult, since you may be writing on that isn't actually sound.
I just think this is a distraction unless your goal is to learn lean and not math.
Errors are found in human proofs all the time. And like everything else, going through the process of formalizing to a machine only increases the clarity and accuracy of what you’re doing.
Over-emphasis on formalism leads me to conclude you just don't understand the purpose of proofs. You are primarily interested in formal logic - not math.
I would invite you to read a few pages of famous papers - for example Perelman's paper on the Poincaré Conjecture.