Comment by empath75

It isn’t but the borrow checker has a formal proof that does need mathlib.