Abstract

Human-oriented theorem proving is the approach to automatic theorem proving that seeks to create algorithms that find proofs in a way that is modelled as closely as possible on how humans find them. It used to be contrasted with machine-oriented theorem proving, where the emphasis was far more on exploiting to the full the vastly superior speed and memory of computers. At the last Big Proof meeting I argued that despite the fact that the machine-oriented approach was more fashionable, it was important not to lose sight of the human-oriented approach. Since that meeting, the whole discussion has been greatly changed by the dramatic developments in AI. I shall argue, but more tentatively, that it is still worth investing significant effort into understanding how human mathematicians find proofs. I shall also report on some of the work my group in Cambridge has been doing in that direction.