The axioms of second order Peano arithmetic are certainly recursively enumerable, in fact you can pick a formulation that only uses a finite number of axioms. And second order arithmetic is much weaker than the type system of Lean, which is probably somewhere between Zermelo set theory and ZFC set theory in terms of proof-theoretic strength.
More generally, I think that computer scientists (in particular PL theorists and type theorists) are much more likely to use powerful logics than mathematicians, with the obvious exception of set theorists.
More generally, I think that computer scientists (in particular PL theorists and type theorists) are much more likely to use powerful logics than mathematicians, with the obvious exception of set theorists.