Abstract: The philosophy of mathematics has long been focused on determining the methods that are appropriate for justifying claims of mathematical knowledge, and the metaphysical considerations that make them so. But, as of late, a number of philosophers have noted that a much broader range of normative judgments arise in ordinary mathematical practice; for example, questions can be natural, theorems important, proofs explanatory, concepts powerful, and so on. Such judgments are often viewed as providing assessments of mathematical understanding, something more complicated and mysterious than mathematical knowledge.

Meanwhile, in a branch of computer science known as “formal verification,” interactive proof systems have been developed to support the construction of complex formal axiomatic proofs. Such efforts require one to develop models of mathematical language, inference, and proof that are more elaborate than the simple foundational models of the last century. In this talk, I will explain how these models illuminate various aspects of mathematical understanding, and discuss ways that such work can inform, and be informed by, a more robust philosophy of mathematics.