If you're interested in interactive theorem proving with Lean (and not condensed mathematics), the Lean community landing page is a good place to start. https://leanprover-community.github.io/

Especially the "Natural Number Game" under "Learning resources" has been successful in teaching folks the very basics for writing proofs. Once finished, a textbook like "Theorem Proving in Lean" can teach the full basics. Feel free to join the Lean Zulip at any point and ask questions at https://leanprover.zulipchat.com/ in the #new members stream.

Mathlib has plenty of contributions from interested undergrads :)