Mechanical Mathematicians A new generation of automatic theorem provers eliminate bugs in software and mathematics.

For several decades, the focus of research in automated deduction was on developing theorem provers—such as resolution provers and satisfiability (SAT) solvers—for classical first-order logic and weaker logics. Recently, there has been more work on developing higher-order automatic theorem provers. These are based on higher-order logics, which support functions as arguments, quantification over functions, and binders (e.g., the notations for summation and integration). These logics are more suitable than first-order logic for expressing a wide range of mathematics, and they are useful for hardware and software verification as well. Recent successes lead us to envision a world in which mathematicians and computer scientists can develop computer-checked proofs faster than L A TEX proofs.