Yeah, I also only learned natural deduction, until I got to the languages course and the professor told us “this is similar to natural deduction, but different”.

Personally I don’t like lean, I prefer coq. But that’s mostly the vibes, both are actually fine. Lean doesn’t do constructive logic, it does classic logic, but you have to give up program extraction for that. That’s why mathematicians are head over heels for lean.