Computers, Reasoning and Mathematical Practice

Computer aided formal reasoning, mathematical assistants which check complex arguments and automated proofs of new and interesting mathematical results have been part of the dream of computational logic for many years. This dream is in part being realised by the success of endeavours such as the Mizar project [110], which has produced many volumes of formalised mathematics, and McCune’s recent proof of the Robbins conjecture [79], cited, along with autonomous vehicle guidance and the chess program Deep Blue, as one of the five most significant achievements of artificial intelligence [114]. Yet it is still the case that few mathematicians use such programs, and their impact outside certain specialised communities has been less than might have been hoped.