Abstract

We begin by discussing which aspects of the ZFC foundation for mathematics are useful for supporting mathematical practice. We focus in particular on those aspects which cater specifically to human styles of mathematical reasoning. We then consider some advantages of categorical or type theoretic foundations, and how these advantages rely on less human-friendly features of those systems. We close by raising the possibility that this latter type of foundation may become more appropriate as mathematical practice shifts towards a greater reliance on computers.