When the author was a boy, he wrote a universal theorem prover. Given enough time and memory, it would prove every theorem in large parts of mathematics. Strangely, this did not put all mathematicians out of business.
The author spent most of his days prior to going off to study at a series of American universities in Germany. That country held annual nation-wide science competitions for secondary school students under the title Jugend Forscht
Translating as Young Scientists
or Youth Do Science.
. Unlike American schools’ science fairs, which challenge students merely to reproduce some well-known results from basic scientific experiments, Jugend Forscht (and its junior division Schüler Experimentieren
for the under-15 crowd) asks participants to come up with and investigate original ideas in mathematics, physics, chemistry, biology, or engineering. The results are judged based on originality, success, and potential usefulness.
Projects ranged from the extremely practical to the completely theoretical. One example of the former that sticks in the mind was a competitor’s ingenious attempt to solve the problem of cars’ high beams. On the one hand, drivers on dark roads wish to turn on their high beams for improved visibility. On the other, the glare from high beams may blind the drivers of oncoming cars. The solution was based on a novel material that could electronically adjust the polarization of the light permitted to pass through it. Apply this material to the headlights and windshield of all cars and adjust the polarization based on the compass direction the car is heading. Now the reflected light from high beams can penetrate the windshield of the driver’s car and provide excellent illumination. However, an oncoming car will have the opposite compass direction and a windshield with the opposite polarization and hence will perceive the light of the original car at greatly diminished intensity, avoiding glare. Every time one drives on a dark road one regrets that this invention has not been widely adopted.
During his sixteenth year, the author had been utterly captivated by Douglas Hofstadter’s Gödel, Escher, Bach.
The author would not go to school, to bed, or to social gatherings without that tome at hand, and whenever there was a moment to spare would sneak off to reread some passage from it. The book is one of a handful which perceptively rewires the reader’s mind in such a way that henceforth it becomes impossible to think about a large variety of phenomena in any manner except its terms. Any gentle reader so inclined should give copies to any teenage acquaintance with an aptiude for and inclination towards a career in mathematics, the more serious sort of philosophy, or any related field; it may be the finest present they ever receive.An excellent supplement are the many marvelous books of logical puzzles by Raymond Smullyan.
As a consequence, the author choose to write a universal theorem prover as his Jugend Forscht project for that year. The computer program would be given the Peano axioms capturing the essence of the natural numbers (i.e., zero and all positive integers) and the generally accepted modes of logical deduction.The process is quite similar to the one described in an earlier post. From these bases, it could derive all the theorems (i.e., all provable truths) about the natural numbers, such as, for example, the infinitude of primes. However, it was not limited to natural numbers, for all the other common sets of numbers and their properties can be constructed from the natural numbers: the modular numbers as equivalence classes between natural numbers, the integers as equivalence classes of pairs of naturals numbers, the rationals as equivalence classes of pairs of integers, the reals as Dedekind cuts of the rationals, the complex numbers as pairs of reals, and so on. So the program would produce all provable truths, such as the Riemann hypothesis or its negation (if either is provable), about these sets of numbers too.
Given such a program, why is mathematics still practised? Because the program was undirected. One could not give it a theorem and then expect to receive back a proof in a reasonable amount of time. Rather, the program produced all of the infinite set of theorems, almost all of which are completely useless, in a nearly random order. It is true that it eventually would produce every theorem, but few useful results could be expected in less time than the age of the universe or with fewer bits of memory than the number of atoms in the universe. In short, the program was merely a cute, but practically useless idea. So we still need mathematicians.
