> Metamath is a proof system, but unlike most alternative systems like Lean, it doesn't have a built-in set of axioms - you need to declare your axioms, and then you can prove theorems (using only previous axioms and proven theorems). So you can declare the axioms of New Foundations, and then use them to prove other things.
I've only used lean a little bit but I'm pretty sure you can start lean with a blank slate, declare whatever you want and then build up from there. In fact the Natural Number Game[1] is basically this, you develop the Peano axioms etc and prove everything about the natural numbers from scratch without using the standard library (which obviously would have all that built in).
No, Lean is not suitable for axiomatic investigations, it comes with too much baggage from "classical foundations". As Randall said above, Lean is axiomatically much stronger than NF, and that's even with "no axioms"! You can use Lean to prove things about axiom systems, but you have to model the axiom system explicitly as a "deep embedding" with syntax and a typing judgment. For metatheory work like the one reported on here this is exactly what you want, but if you want to actually work in the theory then it's an extra layer of indirection which makes things a lot more cumbersome compared to using Lean's own logic.
Metamath is much more configurable in this regard, you just directly specify the axiom system you want to work in and there is no special status given to first order logic or anything like that.
I've only used lean a little bit but I'm pretty sure you can start lean with a blank slate, declare whatever you want and then build up from there. In fact the Natural Number Game[1] is basically this, you develop the Peano axioms etc and prove everything about the natural numbers from scratch without using the standard library (which obviously would have all that built in).
[1] https://adam.math.hhu.de/#/g/leanprover-community/NNG4