This forms part of the Programme on Big Proof This programme (https://www.newton.ac.uk/event/bpr) will gather mathematicians interested in employing proof technology in their research, logicians exploring pragmatic and foundational issues in the formalisation of mathematics, and computer scientists engaged in developing and applying proof technology. This invited talk (https://www.newton.ac.uk/seminar/20170714113012301) will discuss the use of interactive theorem proving in the investigation of historical mathematics. This article was published on 2024-11-22