  Euclid pioneered the concept of a mathematical theory developed from axioms
by a series of justified proof steps. From the outset there were critics and
improvers. In this century the use of computers to check proofs for correctness
sets a new standard of rigor. How does Euclid stand up under such an
examination? And what does the exercise have to teach us about geometry,
mathematical foundations, and the relation of logic to truth?
