The overarching aim of this project, which lends itself to multiple subprojects, is to analyse how humans think about mathematics, and in particular how they discover proofs, with the aim of understanding their thought processes well enough to automate them. This approach, sometimes referred to disparagingly as “good old-fashioned AI”, contrasts with the so-called machine-oriented approach, which aims to find proofs by exploiting the power of computers to perform large searches quickly. It might seem perverse not to use this power, but a good reason for not doing so is that large searches cannot be composed more than a tiny number of times without it leading to a combinatorial explosion. Since the depth of the search tree of a human mathematician is typically large, it seems likely that in order for computers to be able to find the kinds of proofs that humans excel at finding, at some point the question of how to avoid large searches must be confronted, and this is easier to do so with simple problems, even if machine-oriented approaches can already solve those problems. In short, a human-oriented approach is more likely to scale up.