## 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…)