Computational Aspects of Combinatorial Theorems – ACTC

Reverse mathematics are a foundational program at the intersection of computability theory and proof theory, whose aim is to determine the computable strength of axioms necessary to prove ordinary mathematics. This program enabled to reveal a structural phenomenon of mathematics from a computational viewpoint, that is, the vast majority of ordinary theorems is equivalent to one of five big systems of axioms. Despite the success of this program and the growing interest of the scientific community, the computable analysis of a sub-field of mathematics related to Ramsey theory presents some unexpected difficulty. A large part of modern reverse mathematics, and of computability theory in general, focused on this problematics, yielding the development of new techniques and new subfields in computability. Many results concerning the computational content of principles have been gathered, and enabled the development of a methodology of computational analysis over these statements, together with a relative understanding of the deep computational nature of these statements.

The precision of these techniques have led us to believe in the existence of a strong structure ruling the computational content of these combinatorial principles. However, the permissive nature of computational phenomena often enables to construct artificial counter-examples invalidating the strong observations made on the natural principles considered. Our ANR project aims at giving a formal framework to the heuristics used by the community, by proving general theorems. To achieve this, it will be necessary to develop a theory of naturality in computability, to restrain the considered problems to a subclass of so-called "natural" problems, satisfying the observed structural properties. This project will also allow us to reinforce the visibility of computability theory in France, by organizing a summer school and an international conference assembling the experts in reverse mathematics, and more generally in computability theory.