Dear Children,
Do you know that until fifty years ago most of mathematics was done by humans? Even more strangely, they used human language to state and prove mathematical theorems. Even when they started to use computers to prove theorems, they always translated the proof into the imprecise human language, because, ironically, computer proofs were considered of questionable rigor!
Only thirty years ago, when more and more mathematics was getting done by computer, people realized how silly it is to go back-and-forth from the precise programming-language to the imprecise humanese. At the historical ICM 2022, the IMS (International Math Standards) were introduced, and Maple was chosen the official language for mathematical communication. They also realized that once a theorem is stated precisely, in Maple, the proof process can be started right away, by running the program-statement of the theorem.
All the theorems that were known to our grandparents, and most of what they called conjectures, can now be proved in a few nano-seconds on any PC. As you probably know, computers have since discovered much deeper theorems for which we only have semi-rigorous proofs, because a complete proof would take too long.
All the theorems in this textbook were automatically discovered (and of course proved) by computer. The discovery program started with 3 generic points in the plane, and iteratively constructed new points, lines, and circles using a few primitives. Whenever a new point (or line, or circle, or whatever) coincided with an old one, a "theorem" was born. Then a search in Eric's Math Treasure Trove, version 1998, was performed, to see which of the theorems that were discovered by the Discovery Program were anticipated by humans; the program then automatically attached the human names to the theorems. Not surprisingly, all the theorems that turned out to be anticipated by humans, and that are presented in this very elementary textbook, were of very low complexity and depth.
HOW TO USE THIS TEXTBOOK:
You don't have to read it all. Pick any theorem from the Index of Theorems. All the definitions used can be read by clicking on them. These definitions, in turn, may involve other definitions, also clickable, etc. Don't worry, none of the definitions are circular. Definition TS is recursive, but not circular.
Example:
Napoleon's theorem,
involves two definitions:
ItIsEquilateral
and
CET.
ItIsEquilateral
involves
DeSq. DeSq is
primitive.
CET uses
Circumcenter,
Circumcenter involves
the primitive definitions
Ce,
and
Center.
Hence in order to understand the statement
of Napoleon's theorem you only need to look up the definitions: Ce, Center,
CET, Circumcenter, DeSq and ItIsEquilateral,
and get a completely self-contained
statement of the so-called Napoleon Theorem. Then to prove it,
first download
RENE.txt, then
get into
Maple by typing: "maple
If you want to draw other diagrams for any of the theorems, use the
package
PictRENE.txt. To get general help, type:
ezra();, and to get specific help, say, for drawing diagrams for
Napoleon's theorem, type: "ezra(NapoleonP);".
Notes: Points are represented as lists of length 2. Lines are
represented as a*x+b*y+c. Many theorems are proved for the
"standard triangle"
Te(m,n). Of course every triangle is
equivalent to Te(m,n), so there is no loss of generality.
Also all the other simplifications are without loss of generality.
WARNING: x and y are global variables!