Formalization of Cohomology Theories (23w5124)


(University of Alberta)

Anne Baanen (Vrije Universiteit Amsterdam)

(University of South Carolina)

Johan Commelin (Freiburg University)

Heather Macbeth (Fordham University)


Group Photo

The Banff International Research Station will host the "Formalization of Cohomology Theories" workshop in Banff from May 21 to May 26, 2023.

Mathematicians and computer scientists have been collaborating for years to build libraries of mathematical definitions and proofs that can be understood and checked by computers. These formalization efforts have now progressed to cover a substantial portion of an undergraduate and graduate-level mathematics education, with the aspiration to one day include all the ingredients that a modern mathematician needs for their research.

Homology and cohomology are two related sets of theories that are essential to several branches of modern mathematics including algebraic geometry, algebraic topology, etc. The first formalizations of (co)homology have recently been completed, and the time is ripe to add the full spectrum of (co)homology theories to the formal libraries. This workshop aims to bring together experts in formalization and experts in various mathematical areas to advance the state of formalization closer to the leading edge of mathematical research.

Workshop Report - View here

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).