Big Proof – Challenges in Industry and Research

Date: 19 July 2017

Time: 10:00-19:00






This workshop is in collaboration with Turing Gateway to Mathematics.

Please note, there is a £50 registration fee for non-academics for this event.

Proof systems have been used as constructive demonstrations of mathematical validity for millennia, and are now being implemented on computers as “formal proofs”. The generally agreed criteria for formal proofs are that they should have reproducibility (easily accessible and communicable), objectivity (accurately representative) and have verifiability (it being possible to recognise that something is a proof).


The aim of the workshop is to promote discussion around the area of big proof and formal verification, and the challenges from academic and industry perspectives.  For example, academic challenges are presented by the problem of scaling mathematical proof on machine, including issues such as search, representation and reasoning in ways that are more natural to working mathematicians than current systems offer.  Conversely, industry challenges may be posed around the limits of automation and the efficiency of current logic’s and algorithms.

The programme of talks will feature both academic and industry speakers and will include:

  • Verification for mainstream software and security
  • Bringing big verification proof to big finance
  • Big proofs from social networks of mathematics
  • Reasoning with big code
  • Reasoning at scale for cloud computing security

This workshop will be of interest to individuals from research, business and industry communities, who are interested in areas of big proof and formal verification. Relevant sectors include engineering, computer hardware and software, security and finance.