Computer-Assisted Proofs

Using Cutting-Edge Technology to Solve the Most Advanced Problems

Nov 7, 2008

Much of mathematics, both theoretical and practical, has been built up throughout the centuries in the language of proofs - formal statements of mathematical reasoning.

Anyone who has taken a course in geometry or analytical mathematics in school has certainly come across mathematical proofs in one form or another, whether it is a simple proof with just a few basic steps to prove that two triangles are congruent or a multifaceted, in-depth proof that pi is an irrational number. For mathematicians, the language of proofs is nearly as important as learning what "+" and "-" mean.

The Difficulty of Modern Proofs

A proof is, essentially, an attempt to demonstrate the validity of a given notion using words - by telling the "story" of how one came to this knowledge.

Ideally, every mathematical proof would be a "formal proof," that is, a proof which begins at the very beginning, with the most basic unquestionable axioms of mathematics (such as Euclid's five axioms of geometry), and then moves forward logically from there, using simple language in a step-by-step process: "Because so and so is true, then so and so must also be true, which leads to the conclusion that..."

The difficulty in creating these formal proofs lies in the fact that modern theoretical mathematics has become so complicated, and has grown so very much from those initial axioms, that often times it seems quite nearly impossible to list every step that was required to reach a certain conclusion.

For this reason, most modern proofs could be considered, at best, abridged versions of formal proofs. They assume a certain amount of knowledge on the part of their reader, skip over some of the most obvious statements, call upon previous proofs ("As Mr. _____ has previously shown in his proof of right triangles..."), and seek only to bridge those gaps which are directly relevant to what is being proven, leaving certain other steps unspoken.

While there is certainly logic to this methodology - it would be terribly wasteful to force mathematicians to spend countless hours (or weeks or months or years depending on the difficulty of the problem) sorting out every last detail for every proof, especially when those details have already been sorted out by many mathematicians before. Still, mathematical formalism suggests that it would be ideal for every mathematical proof to be formally declared, rather than glossed over.

Technology Comes to the Rescue

The answer to this problem, of course, lies in modern technology. Computers - essentially instruments of logic and proof on their own - are clearly much faster than humans at sorting out complicated arguments. Added to this the fact that mathematical proofs, like computers, essentially follow certain rules of language (if/then statements, because/therefore, etc.), it should also be possible to program computers to use this logic to perform more analytical mathematical operations.

The difficulties in this should be equally as obvious. Mathematicians do not always follow perfectly valid logical reasoning. Often conclusions are jumped to using human intuition which may be beyond the scope of a computer to emulate.

Still, great progress in this area has been made, as has been reported recently by four groundbreaking articles:

Discussed in these articles are the many wonderful advances which have been occurring in computer technology in recent years, specifically focusing both on exactly what constitutes a formal proof, and how mathematicians and computer scientists alike have been working on adapting this language for use in computers. For if a formal set of instructions could be arrived at which allowed the computer to, as much as possible, emulate human mathematical reasoning, great new worlds could be opened up which allow even the most complex of mathematical questions to be answered.

Computers have once again demonstrated that the possibilities of technology are far beyond human reckoning.

The copyright of the article Computer-Assisted Proofs in Math/Chaos Theory is owned by Isaac M. McPhee. Permission to republish Computer-Assisted Proofs in print or online must be granted by the author in writing.