This talk will present a working mathematician's case that this might be an opportune moment to revisit our foundation system to (i) bring the foundations closer to our intuitions and thus (ii) make mathematics easier to formalize. Part of this conviction derives from my experience teaching intro to proofs, while another part arises from my work on $\infty$-category theory. If mathematics is the art of giving the same name to different things, then a flexible notion of identification "=" — which specializes to the correct notion of sameness for higher mathematical structures and is respected by all constructions in the formal system — should be a core foundational concept. I'll explain how homotopy type theory realizes this vision and describe work in progress on computer proof assistants that compute with the univalence axiom.