Mike Gordon is Professor of Computer Assisted Reasoning at the University of Cambridge Computer Laboratory.
Mike Gordon is Professor of Computer Assisted Reasoning at the University of Cambridge Computer Laboratory. For the special issue of Philosophical Transactions A celebrating the 350th anniversary of the journal, he has written a commentary on one of the pioneering papers from our archive, Robin Milner’s paper on ‘The use of machines to assist in rigorous proof’ (1984). Here he answers a few of our questions.
Why was this a landmark paper?
Milner’s research revolutionised the architecture of computer software for mechanically generating and checking mathematical proofs, particularly those needed to establish the correctness of hardware and software designs. The paper was the first to focus specifically on his general theory of problem solving implemented by such software.
How has the use of computers in mathematics developed in the 30 years since Milner’s paper was published?
The last thirty years show that Milner’s ideas have had an enormous impact on the development of programs for checking complex mathematical proofs and proving the correctness of hardware and software designs. In 2014 a proof by Thomas Hales of the Kepler conjecture on packing spheres was checked using software directly descending from Milner’s early proof assistants. Human mathematicians had been unable to check Hales’ proof due to its enormous complexity.
What is an example of how Milner’s work having an impact today?
A recent influential research monograph on the hot topic of homotopy type theory intriguingly states “much of the material presented here was actually done first in the fully formalised setting inside a proof assistant, and only later ‘unformalized’ to arrive at the presentation you find before you — a remarkable inversion of the usual state of affairs in formalised mathematics”.
Did you discover anything surprising when researching this paper?
Milner played the oboe and considered a career as a professional musician. He decided against this because he thought he might need to compose music, which was something he didn’t do.
