Welcome to the blog, Reflections on Big Proof!

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:

1. Novel pragmatic foundations for representing mathematical knowledge and vernacular inspired by set theory, category theory, and type theory.
2. Large-scale formal mathematical libraries that capture background knowledge spanning a range of domains.
3. Algorithmic and engineering issues in building and integrating large-scale inference engines.
4. The social exploration and curation of formalised mathematical and scientific knowledge.
5. Educational proof technology in support of collaborative learning.

Our reflections can direct any of these or other challenges. The benefit of the blog format is that we'll be able to continue the discussion in the comments.

I'll mainly be acting as a host, but I also plan to submit an entry of my own. To post an entry, just email it to me, and I'll post it on your behalf.