New Frontiers in Proofs and Computation (21w5156)


Mathias Baaz (Vienna University of Technology (Austria))

Yong Cheng (Wuhan University)

(Darmstadt University of Technology)

Michael Rathjen (University of Leeds)


The Banff International Research Station will host the "New Frontiers in Proofs and Computation" workshop in Banff from STARTDATE to ENDDATE.

%IMPORTANT: please use the following packages in the preamble: %\usepackage{amssymb,amsmath,amsrefs}

Mathematics distinguishes itself from physics and the other exact sciences by at least two features: adherence to rigorous proofs} and ever-expanding \emph{abstraction beyond physical reality and even itself.
Uniting these two features, proof theory} is the \emph{abstract study of proofs as mathematics objects, pioneered by the famous mathematician David Hilbert around 1900.
This study has unveiled a deep connection between proofs and computation, and our workshop focuses on three related topics in this connection:

  1. \small New organic connections between proof theory and mathematics (proof mining).
  2. The logical strength of formal systems underlying proof assistants.
  3. Human computer programs from proofs (program extraction).

This workshop is dedicated to Hao Wang, for his pioneering work in connecting human and formal thinking that permeates (O1)-(O3).
A greater understanding of these topics will no doubt lead to a better understanding of computation in mathematics and computer science, and increase the prominence of mathematical logic and proof theory in China, Asia, and the world.

The Banff International Research Station for Mathematical Innovation and Discovery (BIRS) is a collaborative Canada-US-Mexico venture that provides an environment for creative interaction as well as the exchange of ideas, knowledge, and methods within the Mathematical Sciences, with related disciplines and with industry. The research station is located at The Banff Centre in Alberta and is supported by Canada's Natural Science and Engineering Research Council (NSERC), the U.S. National Science Foundation (NSF), Alberta's Advanced Education and Technology, and Mexico's Consejo Nacional de Ciencia y Tecnología (CONACYT).