Imagine you are trying to stack up oranges in the most efficient way possible – this means being able to pack the oranges together as densely as possible. In 1611 Johannes Kepler stated that it would be the arrangement which is often favoured by fruit sellers – i.e. putting each sphere on top of a gap in the layer of fruit underneath. This may seem like an obvious solution, however it turned out to be very difficult to prove. A proof needs to show that there is no other arrangement which will be more efficient.
Thomas Hales’ Proof
In 1998 mathematician Thomas Hales presented a proof of what is now known as the Kepler Conjecture. The only problem was that it turned out to be such a long proof that it took 12 other mathematicians four years to check it. Even after all that effort the mathematicians could only say that they had 99% confidence in the proof. The whole point of proof is that it is 100% watertight, so being only 99% sure was simply not good enough.
Computer checking
Thomas Hales was not to be defeated. Instead he translated his proof into the language of formal logic. This meant that he could then use a computer program to formally check his proof, and in 2017 the proof was finally accepted by the mathematical community. In the New Scientist Alan Bundy wrote “A world-famous mathematician has turned his hand toward automated theorem proving, that kind of sociological fact is very important. This is a case study which could start to become the norm.”
Thomas Hales has shown that computers can check very complicated mathematical proofs, and in the future we may begin to see much more of this happening.
Mathematician Thomas Hales and the optimal stacking of spheres.
The Four Colour Theorem
It is also now well known that some mathematical theorems can be proven by computers. The first major theorem to be solved by computer was the Four Colour Theorem in 1976. This Theorem essentially states that you will always be able to colour in a map, in such a way that no two adjacent regions share the same colour, by using at most four colours. It has now been shown that computers can not only create mathematical proofs, but that they can check them as well.
Fortunately for mathematicians, creating new mathematics is a highly creative process and most new mathematics still requires human input. It is however likely that computers will be used more often to complement the work of mathematicians, both in creating proofs and subsequently checking them.
Article by Hazel Lewis
