Formal Proof Assistants (FPAs) are increasingly used in contemporary mathematics, thereby introducing new issues for the Philosophy of Mathematical Practice (PMP) to address. A question arises as to whether these tools may require a reassessment of established standards of mathematical knowledge and related concepts. This presentation will focus on one such issue: What does it mean for a proof constructed within an FPA to be considered rigorous.
The talk will begin by providing an overview of the general philosophical challenges that FPA-based practices present. Following this, a more systematic engagement with the literature on rigor will be developed through the lens of FPAs.
On the one hand, I will argue that FPAs can be accounted for as rigorous according to various accounts of rigor found in the literature: the standard view, argumentative and dialogical models of proof, the recipe model of proof, and virtue-theoretic accounts of rigor (Tanswell, 2024). This will offer a richer description of FPAs.
On the other hand (and this is a work-in-progress project), I will scrutinize the connections between these different accounts and sketch an attempt to unify them in a nuanced version of the standard view. This is intended to reassess existing theories in the PMP to better accommodate practices involving emerging tools.