Philosophers since Thales have demanded valid proofs as the litmus test for the acceptance of a mathematical conjecture as a demonstrable fact. Dually, counterexamples have served as evidence for the demonstrable falsity of a claim. Euclid's codification of the rules of geometry proofs became the paradigm for a foundation for reliable knowledge. With Ramon Llull and Gottfried Leibniz came the idea of mechanizing reason with the unreasonable expectation that this would spark religious and political harmony. The quest for the automation of mathematical reasoning came into sharp focus through the Hilbert's second and tenth problem. The Entscheidungsproblem posed by Hilbert and Ackermann was answered negatively by Church and Turing. The work of logicians in the first half of the 20th century laid the foundation for the development of early theorem-proving programs in the fifties. Skipping ahead, by the dawn of the eighties, automated reasoning had a niche position within the field of artificial intelligence but was still regarded with amusement by outsiders as a somewhat quixotic quest to discover the holy grail of problem solving. We describe the experience of sharing a ringside seat to the growth and maturation of the field of automated reasoning during the last four decades into an integral sub-discipline of computing and a vehicle for the large-scale formalization of mathematical and computational knowledge.