Investigation will be continued for building more powerful computer programs for proving theorems in mathematics. 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.
