This project is part of an ongoing effort to build more powerful computer programs for proving theorems in mathematics and application areas. The work can be divided into subareas: building provers with large-step capacity; using analogy to aid in proof discovery; combining known methods for new proofs in higher order logic; and mechanical methods for streamlining proofs.
