MACHINEPROOFSINGEOMETRY
                Automated Production of Readable Proofs for Geometry Theorems
                           Shang-Ching Chou
                        Department of Computer Science
                         TheWichita State University
                            Xiao-Shan Gao
                         Institute of Systems Science
                          Academia Sinica, Beijing
                           Jing-Zhong Zhang
                      Chengdu Institute of Computer Application
                         Academia Sinica, Chengdu
                        WorldScientific
                            1994
                          ¨
              To WuWen-Tsun
                            v
        Foreword
         Polya named Descartes’ Rules for the Direction of the Mind his favorite book on how
        to think. In the Rules, Descartes speculates on the possible existence of a powerful, secret
        methodknowntotheancientsfor doing geometry:
           Butmyopinionisthatthesewritersthenwithasortoflowcunning,deplorable
           indeed, suppressed this knowledge. Possibly they acted just as many inventors
           are known to have done in the case of their discoveries, i.e., they feared that
           their method being so easy and simple would become cheapened on being
           divulged, and they preferred to exhibit in its place certain barren truths, deduc-
           tively demonstrated with show enough of ingenuity, as the results of their art,
           in order to win from us our admiration for these achievements, rather than to
           disclose to us that method itself which would have wholly annulled the admi-
           ration accorded.
         Descartes, that master of both method and geometry, would have been amazed to see
        the publication of this volume by Chou, Gao, and Zhang, who here present a method for
        provingextremelydifficulttheoremsingeometry,amethodsosimpleandefficientitcanbe
        carried out by highschoolstudentsorcomputers. Infact, themethodhasbeenimplemented
        in a computer program which can prove hundreds of difficult theorems and moreover can
        produce simple, elegant proofs. In my view, the publication of this book is the single most
        importanteventinautomatedreasoningsinceSlagleandMosesfirstimplementedprograms
        for symbolic integration.
         All too often, research in automated reasoning is concerned with technical questions of
        marginal interest to the mathematics community at large. Various strategies for efficient
        substitution and propositional or equational reasoning have dominated the field of auto-
        mated reasoning, and the mechanical proving of difficult theorems has been a rare event.
        Mechanical searches for the proofs of difficult theorems are usually guided extensively by
        the ‘user’. Almost never do we find exhibited a computer program that can routinely treat
        hard problems in any area of mathematics, but in this book we do! The skeptical reader is
        urged to flip through the 400 difficult theorems in Chapter 6, all mechanically proved, and
        try his hand. The exceptional simplicity of the mechanically generated proofs presented for
        many of these theorems illustrate that the authors’ method is not some algorithm of mere
        “in principle,” proof-theoretic relevance, such as Tarski’s method. No, by applying the
        simple method formulated by the authors, the reader may also quickly become an expert
                          vii
            viii                                               Forward
            at geometry proving. The stunning beauty of these proofs is enough to rivet the reader’s
            attention into learning the method by heart.
              The key to the method presented here is a collection of powerful, high level theorems,
            suchastheCo-sideandCo-angleTheorems. Thismethodcanbecontrastedwiththeearlier
            Wumethod,whichalsoprovedastonishinglydifficult theorems in geometry, but with low-
            level, mind-numbing polynomial manipulations involving far too many terms to be carried
            out by the human hand. Instead, using high level theorems, the Chou-Gao-Zhang method
            employs such extremely simple strategies as the systematic elimination of points in the
            order introduced to produce proofs of stunning brevity and beauty.
              Althoughtheoremsaregenerallyregardedasthemostimportantofmathematicalresults
            by the mathematics community, it is methods, i.e., constructions and algorithms, that have
            the mostpractical significance. For example, the reduction of arithmetical computationto a
            mechanicalactivityistherootofthecomputingindustry. Wheneveranareaofmathematics
            can be advanced from being an unwieldy body of theorems to a unified method, we can
            expect serious practical consequences. For example, the reduction of parts of the calculus
            to tables of integrals and transforms was crucial to the emergence of modern engineering.
            Although arithmetic calculation and even elementary parts of analysis have reached the
            point that computers are both faster at them and more trustworthy than people, the impact
            of the mechanization of geometry has been less palpable. I believe this book will be a
            milestone in the inevitable endowment of computers with as much geometric as arithmetic
            prowess.
              Yet I greet the publication of this volume with a tinge of regret. Students of artifi-
            cial intelligence and of automated reasoning often suffer from having their achievements
            disregarded by society at large precisely because, as Descartes observed, any simple, in-
            genious invention once revealed, seems first obvious and then negligible. Progress in the
            automation of mathematics is inherently dependent upon the slow, deep work of first rate
            mathematicians,andyetthisfundamentallyimportantlineofworkreceivesnegligiblesoci-
            etal scientific support in comparison with those who build bigger bombs, longer molecules,
            or those multi-million-line quagmires called ‘systems’. Is it possible that keeping such a
            work of genius as this book secret would be the better strategy for increased research sup-
            port, using the text as the secret basis for generating several papers and research proposals
            around each of the 400 mechanically proved theorems, never revealing the full power of
            the method?
                                                     Robert S. Boyer
                                                     December, 1993