# Automated Theorem Proving **Domain:** Artificial Intelligence / Formal Reasoning / Logic **Doc Type:** Discipline Node **Maturity:** Developed **Related:** [[Artificial Intelligence]], [[GOFAI (Good Old-Fashioned AI)]], [[IBM Research]], [[Gottfried Wilhelm Leibniz]] ## Definition **Automated theorem proving** develops computational methods for constructing or verifying mathematical proofs from formal axioms and inference rules. ## IBM Geometry Theorem Machine In 1959, an IBM 704 running a program of roughly 20,000 instructions proved its first theorem in elementary Euclidean plane geometry. Work by Herbert Gelernter, J. R. Hansen, D. W. Loveland, and colleagues combined symbolic axioms with information derived from diagrams to guide search. The result belongs to the pre-Yorktown history of IBM machine intelligence. It demonstrates that computers were being used for formal reasoning before the [[IBM Thomas J. Watson Research Center]] opened, while Yorktown later became the headquarters of the research organization carrying that lineage. ## Ontology The field realizes part of [[Gottfried Wilhelm Leibniz|Leibniz’s]] dream of reasoning by calculation, but only inside explicitly formalized domains. A proof system’s correctness does not by itself establish understanding, consciousness, or competence outside its axioms. ## Sources / Provenance - IBM Research, “Empirical explorations of the geometry theorem machine” (1960): https://research.ibm.com/publications/empirical-explorations-of-the-geometry-theorem-machine - IBM Research, “A note on syntactic symmetry and the manipulation of formal systems by machine” (1959): https://research.ibm.com/publications/a-note-on-syntactic-symmetry-and-the-manipulation-of-formal-systems-by-machine