[bokoharambe]

I am currently coasting through a mathematics undergraduate degree after having taught myself how to do proofs using a proof assistant. The last barrier to autodidacticism in mathematics is overcome with them, because one no longer needs direct contact with the mathematical community via academia to learn the techniques used (at the undergraduate level.)

[jhanschoo]

I don't think the math libraries for proof assistants are good enough to support undergrad math very well, but they may be occasionally useful in specific places. I still think you will dominantly be doing informal proofs to make progress with any velocity.

[wheelinsupial]

Which proof assistant did you use?