The central theme of our research is *machine assisted
reasoning*. We carry out research on the formalisation of
mathematics, and the use of proof assistants for the verification and
synthesis of software. A large part of our work is in investigating
new theorem proving technology, and this is applied in the proof tools we are developing. We also have
several other projects related to
mathematical reasoning.

The former name of our research group (which still survives in our
web address) was the *Dream* group, standing for **D**iscovery
and **Rea**son in **M**athematics. The aim was to try and
characterise how mathematicians themselves do proofs, and to put this
understanding to use in a tool or, to put it another way, to take an
`AI approach' to theorem proving. This research is ongoing, and puts
into practice the *proof planning* approach to theorem proving.

Past work in this area has included innovations such as rippling, middle-out-reasoning, critics, as well as work on user interfaces. This research has all fed into the proof planners, IsaPlanner, Lambda Clam, and its predecessor, Clam.

As well as continuing to work on the automated tools, IsaPlanner and Lambda Clam, we also pursue research on interactive theorem proving, using tools developed elsewhere, including Isabelle, Coq and HOL.

Some of the research in the group tackles the problem of formalising certain areas of mathematics, real analysis, in particular, in the Isabelle/HOL theorem prover, and proving substantial amounts of the theory therein. There is also work on using the proof planning paradigm to automate some of these proofs.