Introduction to Shalosh B. Ekhad XIV's Geometry Textbook

 
# INTRODUCTION: 
# 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 cover-to-cover. Pick any theorem
# in Part I, and then look up, in Part II, the definitions used in the
# statement-program of that theorem.
# These definitions, in turn, may involve other definitions, etc.
# Don't worry, none of the definitions are circular.
##
## Example: Look up Napoleon's Theorem. It involves two definitions:
# ItIsEqui and CET. Look up ItIsEqui. It involves DeSq. DeSq is
# primitive. Now look up CET. It uses Circumcenter. Circumcenter involves
# the primitive definitions Ce and Center. Hence to understand the statement 
# of Napoleon's theorem you only need to look up the definitions: Ce, Center,
# CET, Circumcenter, DeSq and ItIsEqui, and get a completely self-contained 
# statement of the so-called Napoleon Theorem. Then to prove it, get into 
# Maple by typing: "maple" (without the quotes); once inside Maple, 
# type: "read text;" (without the quotes), and then "Napoleon();" 
# (without the quotes). You should immediately get the response of the 
# computer: true.
##
##
## Note: A point is represented as a list of length 2.  Lines are
## represented as a*x+b*y+c.
## WARNING: x and y are global variables!
###
### Note From the Downloader (DZ):
## IMPORTANT: THIS TEXTBOOK IS ALSO AVAILABLE ON-LINE AS A MAPLE PACKAGE
## CALLED "RENE", FROM http://www.math.rutgers.edu/~zeilberg/
## (click on "Maple packages and programs", then click on "RENE").
## This textbook was tested for Maple V, ver. 5 and previous versions.
## Unfortunately, every year or so, Maple comes out with a new version
## (bigger but not always better, and sometimes buggier)
## that is not fully compatible with code written for previous versions.
## The package RENE will be constantly updated to conform to future
## versions, but let's hope that Maple will start to become upward-compatible.
## RENE will also be continuously enlarged to include new proofs, in particular
## of Monthly problems and IMO problems (it already has a few now).