Infeasibility of solving finite mathematical problems

Abstract:

I will prove that the decision problem for finite mathematical
statements, though recursive, is infeasible in seemingly any realistic
model of computation. To this end, I will construct a set of finite
mathematical statements which can only be feasibly solved by programs
long enough to explicitly encode a decision for each statement.

This result was published in 1973, by Michael Makkai. In this talk I
will show (1) his original proof and its connection to the Gödel
incompleteness theorem and (2) a needed strengthening of his 1973
result.

As time permits, I will also highlight connections to computational
complexity and to algorithmic information theory (Kolmogorov
complexity).