  We report on a project to use a theorem prover to find proofs of the theorems
in Tarskian geometry. These theorems start with fundamental properties of
betweenness, proceed through the derivations of several famous theorems due to
Gupta and end with the derivation from Tarski's axioms of Hilbert's 1899 axioms
for geometry. They include the four challenge problems left unsolved by Quaife,
who two decades ago found some \Otter proofs in Tarskian geometry (solving
challenges issued in Wos's 1998 book). There are 212 theorems in this
collection. We were able to find \Otter proofs of all these theorems. We
developed a methodology for the automated preparation and checking of the input
files for those theorems, to ensure that no human error has corrupted the
formal development of an entire theory as embodied in two hundred input files
and proofs. We distinguish between proofs that were found completely
mechanically (without reference to the steps of a book proof) and proofs that
were constructed by some technique that involved a human knowing the steps of a
book proof. Proofs of length 40--100, roughly speaking, are difficult exercises
for a human, and proofs of 100-250 steps belong in a Ph.D. thesis or
publication. 29 of the proofs in our collection are longer than 40 steps, and
ten are longer than 90 steps. We were able to derive completely mechanically
all but 26 of the 183 theorems that have "short" proofs (40 or fewer deduction
steps). We found proofs of the rest, as well as the 29 "hard" theorems, using a
method that requires consulting the book proof at the outset. Our "subformula
strategy" enabled us to prove four of the 29 hard theorems completely
mechanically. These are Ph.D. level proofs, of length up to 108.
