This Platform Grant supports essential infrastructure and exploratory activities for a portfolio of projects that focus on the automation of mathematical reasoning processes - including their analysis, development and interaction. We can be broadly classified by our holistic perspective of automated reasoning. Central to this theme is the interplay between representation and reasoning. Discovering the right representation can often dramatically simplify the reasoning required in solving a problem. Conversely, meta-level reasoning, and in particular proof-failure analysis, can often provide guidance in evolving the right representation. The Platform Grant enables us to maintain and strengthen the momentum that has been build up around this theme - both in terms of basic research as well as applications: The former covers a spectrum of topics, including: cognitive aspects of theory formulation and reformulation; mathematical discovery and automatic theorem generation; ontology creation, repair and evolution; proof procedures; proof planning; AI problem reformulation; quantum computation; computational creativity; visualisation of reasoning processes. The latter covers wide ranging applications such as: software verification; formal modelling of software intensive systems; graphics design; games design; disaster recovery planning. Our work is a unique blend of the techniques of artificial intelligence and theoretical computer science - we also believe we are unique in our holistic perspective of automated reasoning and mathematical discovery.