This sounds very interesting and relevant to the goals of the CSLib initiative that apparently just got started. I don't have a better public link to it now except this LinkedIn post (perhaps there's a Zulip tag):

https://www.linkedin.com/posts/lean-fro_leanlang-cslib-forma...

What will that accomplish?

You can write proofs along with the course, and since they are machine checked you can have confidence that they are correct.

If you don't know, writing a proof in isolation can be difficult, since you may be writing on that isn't actually sound.

Learning math is more about the big ideas. Behind each proof is an insight. Formalizing in a computer is like spell checking a document. It helps you catch small mistakes but doesn’t change the content,

I just think this is a distraction unless your goal is to learn lean and not math.

Hard disagree.

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.

You are correct that mistakes are made all the time - but they tend to be "oh yeah let me fix that right now" mistakes. Or, "oh yeah that's not true in general, but it still works for this case". That's because the experts are thinking about the content of the material - and they are familiar with it enough to tell if an idea has merit or not. Formalism is just a mode of presentation.

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.