Big proof: Recent Episodes
Cambridge University
Proofs as constructive demonstrations of mathematical validity have been at the heart of mathematics since antiquity. Formal proof systems capture the definitions, statements, and proofs of mathematical discourse using precisely defined formal languages and rules of inference. Formal proofs have enabled mathematicians to rigorously explore foundational issues of expressiveness, consistency, independence, completeness, computability, and decidability. The formalisation of proof facilitates the representation and manipulation of mathematical knowledge with modern digital computers. During the last sixty years, the digitisation of formal mathematics has yielded satisfiability solvers, rewriting engines, computer algebra systems, automated theorem provers, and interactive proof assistants. Proof technology can be used to perform large calculations reliably, solve systems of constraints, discover and visualise examples and counterexamples, simplify expressions, explore hypotheses, navigate large libraries of mathematical knowledge, capture abstractions and patterns of reasoning, and interactively construct proofs. The scale and sophistication of proof technology is approaching a point where it can effectively aid human mathematical creativity at all levels of expertise. Modern satisfiability solvers can efficiently solve problems with millions of Boolean constraints in hundreds of thousands of variables. Automated theorem provers have discovered proofs of open problems. Interactive proof assistants have been used to check complicated mathematical proofs such as those for the Kepler’s conjecture and the Feit-Thompson odd order theorem. Such systems have also been applied to the verification of practical artifacts such as central processing units (CPUs), compilers, operating system kernels, file systems, and air traffic control systems. Several high-level programming languages employ logical inference as a basic computation step.
This programme is directed at the challenges of bringing proof technology into mainstream mathematical practice. The specific challenges addressed include
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. This programme brings together 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. The programme includes a week-long workshop exploring foundational, theoretical, and practical challenges in exploiting proof technology to transform mathematical practice across a range of scientific and engineering disciplines. A key expected output is a concrete, long-term research agenda for making computational inference a basic technology for formalising, creating, curating, and disseminating mathematical knowledge in digital form.