The idea of this blog is to collect some reflections and conclusions from the participants of the Big Proof programme which ran at the Isaac Newton Institute in Cambridge from June 26th until August 4th, 2017. As described at the link above, the programme was directed at the challenges of bringing proof technology (proof assistants and automated theorem proving) into mainstream mathematical practice. It listed 5 specific challenges: Novel pragmatic foundations for representing mathematical knowledge and vernacular inspired by set theory, category theory, and type theory. Large-scale formal mathematical libraries that capture background knowledge spanning a range of domains. Algorithmic and engineering issues in building and integrating large-scale inference engines. The social exploration and curation of formalised mathematical and scientific knowledge. Educational proof technology in support of collaborative learning. Our reflections can direct any of these or other challen