Around 1637, Pierre de Fermat, one of the giants of modern mathematics, issued what became the most famous mathematical conjecture in history. In his copy of Diophantus’ Arithmetica, he wrote:
…it is impossible for any cube to be the sum of two cubes, or in general for any number that is a power greater than the second to be the sum of two like powers. I have discovered a truly marvelous demonstration of this proposition that this margin is too narrow to contain.
Expressed in mathematical notation, Fermat’s conjecture states that there are no integers, x, y, and z that satisfy the diophantine equation xn + yn = zn when n is a whole number greater than 2. The challenge to prove or disprove Fermat’s conjecture was enhanced by rewards offered for its solution. In 1815 and 1860, the French Academy of Sciences offered a gold medal and 300 francs for a proof and in 1908, the German Academy of Sciences offered a prize of 100,000 marks—a fortune in pre-inflationary Germany! In spite of these inducements, the conjecture defied proof for more than 350 years. Mathematicians were beginning to believe that this conjecture was one of the dreaded “undecidable propositions” that Gödel had warned about.
On June 23, 1993, Dr. Andrew Wiles of Princeton University completed his final lecture at a Cambridge University Conference with the statement, “I better stop there”. The audience, comprised of the world’s greatest number theorists, was incredulous—paralysed for a few seconds. As the significance of the chalkboard equation registered, the silence gave way to a thunderous applause. It appeared that Wiles had proved Fermat’s conjecture. For the previous 7 years, he had labored in secret, convinced that he could conquer the Mt. Everest of mathematical problems.
In the year following Wiles’ announcement, some astute mathematicians found flaws in the argument. Intense work in the ensuing two-year period, enabled Wiles to amend the attempted proof to remove those flaws. By 1995, there was general agreement among number theorists, that the 130-page revised version was valid, so that Fermat’s conjecture is now referred to as Fermat’s Last Theorem! Wiles’ proof was a herculean task that mathematician John Conway dubbed, “the proof of the century.” For this achievement, he was knighted and in 2016, Sir Andrew Wiles was awarded the Abel Prize.
The proof of Fermat’s Theorem is a sequenced set of logical deductions that link the basic axioms of algebra to the final statement of the theorem. Those who doubt that Watson has closed that gap between machine and human intelligence are asking, “If computers are the equal of humans, could a computer theorem prover verify Wiles’ proof of Fermat’s Last Theorem?”
