Same thing happened to John Milnor.
ivan astikov writes:
> I do get the general gist that there are still problems to be solved though, and
> this leads me to ask - Can these problems be overcome with brute computer
> force? Will there always be new math’s problems, or is it only a matter of time
> and computing power before everything to do with math’s is known?
Here’s an example to show you the difference between an equation to be solved and a theorem to be proved. Both might be described as problems, but they are quite different things. This question go back to the time of the ancient Greeks:
Suppose the question is “What is the square root of 2?” Most people today would think of that in terms of a decimal that’s sufficiently close to the answer. So, for instance, this decimal is pretty close:
1.414213562373095048802
For nearly any physical question, this is far more accurate than what you need. In the days of the ancient Greeks though, they would want an answer that’s a fraction. 7/5 is close to the answer. 2,828,427/2,000,000 is even closer. The ancient Greeks wondered if there is a fraction that exactly equals the square root of 2. They were able to prove that there is no such fraction. This is not saying that we haven’t yet found any fraction. This is not saying that there might be such a fraction, but it has a numerator and denominator so large that no computer we could ever invent could ever find it. This is saying that no fraction whatsoever could be the exact square root of 2.
Here’s the proof of that, and it’s a proof that the ancient Greeks came up with: Suppose there is a fraction which is exactly the square root of 2. That fraction can be expressed in lowest terms. That is, it can be expressed so that there is no common factor of the numerator and denominator. So, for instance, 14/10 isn’t in lowest terms, since 2 divides both 14 and 10. 7/5 is in lowest terms, since no integer (except for 1) evenly divides both 7 and 5. Every fraction can be turned into one in lowest terms.
Now supposed that A/B is the fraction that is the exact square root of 2 expressed in lowest terms. Then:
(A/B)**2 = 2
(Note that **2 means to square a number.)
So then:
(A2) / (B2) = 2
So also:
(A2) = 2 * (B2)
(Note that the * sign means multiplication.)
Look at that last equation. The right side is divisible by 2, so the left side (which is the same number) is divisible by 2. The left side is the square of an integer and is divisible by 2. That means that A must also be an even number. If A was an odd number, its square would be an odd number.
The square of an even number is always divisible by 4. So the left side of the equation is also divisible by 4. This means that B2 is divisible by 2. (If it wasn’t, then 2 * (B2) couldn’t be divisible by 4.) But this means that B is also an even number, since if B was odd, it’s square would be an odd number too.
But we have now proved that A and B are both even numbers. That means that A/B is not a fraction in lowest terms, since both A and B are divisible by 2. So it’s impossible to find a fraction in lowest terms that is the exact square root of 2. Since any fraction can be reduced to lowest terms, that means that no possible fraction is the exact square root of 2.
That was what the ancient Greeks wanted to prove, since they thought in terms of fractions. If you think in terms of decimals, it’s still true, since any (terminating) decimal can be expressed as a fraction.
So if you want the square root of 2, we can write it to any accuracy you want. In older algebra books, in fact, students were taught a simple process (no harder than long division, at least) by which they could calculate with pencil and paper the square root of any number to any accuracy (or at least to any accuracy before their hand fell off from the effort at writing). However, if you want a fraction or a decimal that’s an exact square root of 2, it doesn’t exist. It’s not just not calculable; it simply doesn’t exist.
This is what mathematicians do. They don’t spend their time finding the answer to specific equations. They prove theorems about whether the solution to problems exist. Sometimes they work out ways to find the solution to an equation with as much accuracy as desired in the quickest possible way.
The most famous counterexample of this (and perhaps the only one?) is the proof that all Robbins algebras are Boolean, by the EQP theorem prover (a problem that stumped Tarski for decades).
There’s the four color theorem.
Cool - I did not know that. I was going to mention the computer’s contribution to the proof of the 4-color theorem, but I see ZenBeam beat me to it.
The four color theorem isn’t regarded as quite the same because the proof structure was known; the computer was just needed to do the calculations.
Yeah, the computer aided proof of the four colour theorem isn’t really that remarkable, any more. There’s a whole field of “formal mathematics” that uses proof assistants to write mathematics in, check existing proofs, and check proofs that are way too big to be done by hand (like verifying the design of processors).
For instance, one of my former lecturers checked Hilbert’s Grundlagen in the proof assistant Isabelle, and found Hilbert’s proofs contained many holes. This may not sound all that surprising, but Hilbert’s motivation for developing the Grundlagen was to show that mathematics (specifically geometry, in this case) could be developed purely from an axiomatic base, without any intuition at all. As a result, Hilbert’s proofs were considered extremely formal, by human standards. What was found, however, was that Hilbert was relying on geometric intuition (and on diagrammatic reasoning, which allowed silent assumptions to creep in) in many places, and this only came to light when they the proofs were checked line by line by computer.
Many more examples of proofs like this are available in the Archive of Formal Proof.
The solution to the Robbins problem was slightly different, though. All proofs in Isabelle are still guided by hand—that is, the mathematician working the computer must still know how to prove the theorem, and just uses the computer to check the proof. EQP, however, found the proof all by itself (albeit, it took something like 8 days of continuous computation to find, a testament to the fantastically huge size of the proof search space). This was the first time a significant theorem was shown to hold by a computer, which had stumped human mathematicians for decades.
(Of course, many mathematicians object to this, for good and bad reasons :p)