Analysing Human Proof Processes

Mohan Ganesalingam

This talk will introduce a project (joint with Timothy Gowers) to analyse the way in which mathematicians construct proofs. Our work to date has focused on breaking up simple proofs to try to find the different 'building blocks' which may be used in proofs, and to understand how these are sequenced to solve problems. We put particular emphasis on making sure that our analysis is not just logically valid, but cognitively meaningful -- that is, we aim to break proofs into units which correspond to the thoughts a human mathematician might have when working through a problem.

To test the theory, we have constructed a program that tackles simple problems in abstract analysis, producing human-like, human-readable proofs; some output from this program will be shown in the talk.