Archive for July 28th, 2008

More quasi-automatic theorem proving

July 28, 2008

In this post I shall continue some of the themes of the previous one by looking at fairly simple but not completely trivial mathematical statements and trying to imagine how a computer might systematically solve them. The main one comes later on: I shall look at how a computer might arrive at a construction of an injection from \mathbb{N}\times\mathbb{N} to \mathbb{N}. (If you don’t know what this means, it’s simple to explain: to each pair of positive integers (m,n) one must assign a positive integer f(m,n) in such a way that no two pairs get assigned the same positive integer.) (more…)