New Frontiers in Proofs and Computation (Online) (21w5156)

The Institute for Advanced Study in Mathematics will host the "New Frontiers in Proofs and Computation" workshop in Hangzhou, China from September 12 to September 17, 2021.

Mathematics distinguishes itself from physics and the other exact sciences by at least two features: adherence to rigorous proofs and ever-expanding abstraction beyond physical reality and even itself. Uniting these two features, proof theory is the 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. 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 Institute for Advanced Study in Mathematics (IASM) in Hangzhou, China, and the Banff International Research Station for Mathematical Innovation and Discovery (BIRS) in Banff, are collaborative Canada-US-Mexico ventures that provide 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 in Banff 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).