This presentation explores the “practical turn” in contemporary philosophy of mathematics, focusing on the use of Interactive Theorem Provers (ITPs) and their intersection with artificial intelligence. In mathematical practice, the distinction between knowing-that a proof is correct and knowing-why it is correct is central. Knowing-that refers to the recognition of correctness grounded in evidential reasons (rationes cognoscendi), whereas knowing-why emphasizes conceptual understanding and explanatory reasons (rationes essendi). This distinction is especially relevant in mathematics education, where explanation—not mere verification—is key to fostering deep comprehension and intellectual autonomy.

The rise of ITPs, particularly in an era shaped by AI, raises important questions about the nature of mathematical explanation. While ITPs are highly effective at verifying proofs, their ability to clarify mathematical ideas and support explanation remains contested. This presentation critically examines the extent to which ITPs—alone or with AI tools—can contribute to the explanatory dimension of mathematical practice. Drawing on insights from philosophy, mathematics, and computer science, I assess the potential and limits of these technologies not only for discovering and verifying proofs but also for cultivating understanding and explanation. The discussion aims to clarify the evolving role of ITPs in the explanatory and practical landscape of mathematics.