Technologist - Automated Theorem Proving
I argued in my D.Phil. thesis that when we reason about infinitistic objects in mathematics, we're really reasoning about finite projections of them. I was led to this conclusion by (among other things) the crucial role of pictures in mathematical reasoning.
Diagram for the Schroeder-Bernstein theorem in set theory. We were able to prove the theorem fully automatically from the diagram.
Diagram for the Diamond Lemma, the first theorem we were able to prove fully automatically from the diagram.
After working with computers for a few years, I started wondering: can diagrams help a computer prove theorems automatically? Other researchers were getting interested in diagrammatic reasoning around the same time.
My work - most of it a collaboration with Dave Barker-Plummer - addressed theorem proving in set theory. Some of the results are non-diagrammatic: for example, a lambda-unification algorithm for set theory, and the Z-match inference rule. The diagrammatic work is presented here.