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
no reviews yet
Please Login to review.