## Archive for the ‘Demystifying proofs’ Category

### Finding Cantor’s proof that there are transcendental numbers

December 9, 2010

I’ve just posted a question at Mathoverflow challenging people to come up with examples of proofs that appear to require a sort of “cognitive leap” that humans are surprisingly good at and that it is hard to imagine computers ever being capable of. I don’t myself believe that there is some fundamental way in which humans are better at mathematics than computers are (or rather, could ever be). So this is the first of what may turn into a series, if I have time, of posts in which I shall try to demonstrate that examples that have been suggested are of proofs that a computer program could in principle find too. (Many of the examples suggested are in areas where I have absolutely no hope of doing this: I’m not going to be able to tell you how a computer could have invented Thom’s work on cobordism, for instance.)

In this post I want to tackle a proof that was a pretty radical departure when it first came out: Cantor’s indirect proof of the existence of transcendental numbers.
(more…)

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

### What is deep mathematics?

July 25, 2008

Note added 12/9/09: It seems that many people are looking at this post, because Derren Brown claims to have used “deep mathematics” combined with “the wisdom of crowds” to predict the lottery. All I can say is that this is obvious nonsense. Whatever method you use to predict the lottery, the drawing of the balls is a random process, so you will not improve your chances of being correct. Brown has done a clever trick — I won’t speculate about his methods, as I’m not interested enough in them — but his explanation of how he did it is not to be taken seriously.

In this post I shall discuss the proofs of two statements in real analysis, one of which is clearly deeper than the other. My aim is to shed some small light on what it is that we mean when we make that judgment. A related aim is to try to demonstrate that a computer is in principle capable of “having mathematical ideas”. To do these two things I shall attempt to explain how an automatic theorem prover might go about proving the two statements in real analysis: in one case this is quite easy and in the other quite hard but by no means impossible. In the hard case what interests me is the precise ways that it is hard, which I think say something about the notion of depth in mathematics.
(more…)

### The exchange lemma and Gaussian elimination

October 3, 2007

Thanks to this comment, I have finally decided to try to understand in what sense Gaussian elimination and the Steinitz exchange lemma are “basically the same thing”. It’s not at all hard to spot similarities, but it seems to be a little trickier to come up with a purely mechanical process for translating proofs in one language into proofs in the other.

It might be of some interest to know how I approached this post. Rather than working everything out in advance, I started with an incomplete understanding of the connection. I had thought about it enough to convince myself that I could get to the end, but found that as I proceeded there were a few surprises, and the eventual connection was not quite as close as I was expecting. (Actually, this paragraph is slightly misleading. I am writing it while in the middle of writing the rest of the post. I’ve had a few surprises, and though I am fairly sure I’ll get to the end I am not quite sure what the end will look like. [Note added after I'd got to the end: it was nothing like what I expected.]) (more…)

### One way of looking at Cauchy’s theorem

September 19, 2007

Cauchy’s theorem is the assertion that the path integral of a complex-differentiable function around a closed curve is zero (as long as there aren’t any holes inside the curve where the function has singularities or isn’t defined). This theorem, which is fundamental to complex analysis, can be vastly generalized and seen from many different points of view. This post is about a little idea that occurred to me once when I was teaching complex analysis. I meant to include it as a Mathematical Discussion on my web page but didn’t get round to it. Now, while the novelty of having a blog still hasn’t worn off, I find I have the energy to put it here.

Let’s start with a simpler fact: that if $f$ is a function from $\mathbb{R}$ to $\mathbb{R}$ and the derivative of $f$ is everywhere zero, then $f$ is constant. What is the natural generalization of this fact to functions defined on the plane? (more…)

### Discovering a formula for the cubic

September 15, 2007

In this post I want to revisit a topic that I first discussed on my web page here. My aim was to present a way in which one might discover a solution to the cubic without just being told it. However, the solution that arose was not very nice, and at the end I made the comment that I did not know a way of removing the rabbit-out-of-a-hat feeling that the usual much neater formula for the cubic (together with its derivation) left me with.

A couple of years ago, I put that situation right by stumbling on a very simple idea about quadratic equations that generalizes easily to cubics. More to the point, the stumble wasn’t completely random, so the entire approach can be justified as the result of standard and easy research strategies. I am no historian, but I would imagine that this idea is pretty similar to the idea (in some equivalent form) that first led to this solution. (more…)