Ursula Martin
Professor Ursula Martin CBE FREng FRSE
Room N 3.14, Mathematical Institute
Biography
Ursula Martin joined the University of Oxford as Professor of Computer Science in 2014. She she holds an EPSRC Established Career Fellowship, as a member of the Mathematics Institute and the Department of Computer Science, and is a Senior Research Fellow at Wadham College. She is a Commander of the Order of the British Empire, a Fellow of the Royal Academy of Engineering, a Fellow of the Royal Society of Edinburgh, and also holds fellowships of the British Computer Society and the Institute of Mathematics and its Applications. She is a Doctor of Science honoris causa of the University of London, an Honorary Fellow of Royal Holloway University of London, and holds a PhD and MSc from the University of Warwick, and an MA and BA from the University of Cambridge. She is also a Visiting Professor at the University of Edinburgh.
Before joining Oxford, she held a chair of Computer Science in the School of Electronic Engineering and Computer Science at Queen Mary University of London, where she was VicePrincipal for Science and Engineering (20052009), and Director of the impactQM project (20092012), an innovative knowledge transfer initiative. She served on the UK Defence Science Advisory Council, on the 2001 and 2008 UK HEFCE RAE panels for Computer Science, and was a SICSA distinguished visitor at the University of Edinburgh for 201213. Her career was interrupted for two years by illhealth, and she is grateful to Queen Mary for their support during this time, which enabled her to reorient her research to mitigate the longterm cognitive impact of chemotherapy. She has previously held appointments at the University of St Andrews (the second female professor in any discipline since its foundation in 1411, the first having been appointed in some fifty years before); Royal Holloway University of London; Manchester; and Urbana Champaign. Throughout her career she has been involved in many activities for women in science, most recently serving on the Royal Society's Diversity Committee, and leading research and outreach based on the mathematics of Ada Lovelace. She is involved in many aspects of science policy, currently serving on HEFCE's Interdisciplinary Advisory Panel for the 2021 Research Excellence Framework.
Her research, initially in algebra, logic and the use of computers to create mathematical proofs, now focuses on wider social and cultural approaches to understanding the success and impact of foundational research in computer science and mathematics.
Current research, the Social Machine of Mathematics
Since 2014 her research has been supported by an EPSRC Fellowship investigating cultures of mathematics to understand mathematics as as a social machine. The resulting highly interdisciplinary portfolio of work, using philosophy, social scence and history alongside computer science research in artificial intelligence, argumentation theory and verification, shows the scope for new computer techniques to support concept formation and argument finding, while highlighting the roles that risk, doubt, error, explanation and group knowledge play in the human production and use of mathematics. Current postdocs are Joe Corneli and Lorenzo Lane: former postdocs Chris Hollings (Oxford), Gabriela Nesin (Brighton), Alison Pease (Dundee) and Fenner Tanswell (St Andrews) have moved on to lectureships.
Project workshops included Group knowledge and mathematical collaboration 78 April 2017, and Enabling mathematical cultures 57 December 2017
Other Conferences and seminars
External presentations in 2018 will include: January: AMS Joint Mathematical meetings (History of computing; crowdsourced maths) February: University of Oxford History of Science Seminar (Victorian mathematics); April: University of Oxford [Mathematics Institute, open lecture] (Launch of Ada Lovelace book); June: British Mathematical Colloquium [keynote]; Mathematics and Patronage meeting [keynote]; July: IEEE Logic in Computer Science Conference, Oxford [keynote]
External presentations in 2017 include: January: AMS Joint Mathematical meetings (Ada Lovelace), University of Waterloo [open lecture] (Ada Lovelace); University of Waterloo [Faulty of Mathematics] (Future of Proof); MIT (Mathematical practice); February: University of Kent (Future of Proof); University of Leicester (Ada Lovelace); University of Oxford [Mirzakhani Society] (women in mathematics) April: University of Oxford [Faculty of Philosophy] (Future of Proof); May: University of Oxford [Faculty of English] (Ada Lovelace); University of Oxford [Mathematics Institute, open lecture] (Hidden Figures of Oxford Computing); Birkbeck London [Computer Science] (Future of Proof); June: CIE conference, Turku, Finland [keynote]; University of Glasgow, 60th anniversary of Computer Science Department [keynote]; July: Big Proof workshop, Isaac Newton Institute, Cambridge [keynote]; ICHSTM, Rio de Janiero [history of science] (Impact of mathematics); September: UK Mathematics Trust [school students] (Ada Lovelace); Malvern Girls College and nearby schools [school students]; St Anne's Caversham and nearby schools [school students]; October: University of St Andrews Distinguished Lectures in Computer Science [three open lectures]; Cambridge U3A (Ada Lovelace); Cambridge Computing History Centre (Ada Lovelace); December: Enabling Mathematical Cultures, Oxford [keynote].
Main research themes
Investigation of online mathematical collaboration to understand how proof comes about, and the model provided by social machines, in particular looking at evidence from writings by mathematicians, and from study of online mathematical collaborations
 Martin, Ursula 2016 Computational logic and the social Journal of Logic and Computation, 26, 467477 provides an overview in historical context.
 Martin, Ursula and Pease, Alison 2015 Stumbling around in the dark: lessons from everyday mathematics Springer LNCS, 9195, 29  51 (invited plenary for 25 years of CADE) looks at social machines in the context of formal proof and experimental mathematics
 Martin, Ursula and Pease, Alison 2015, Hardy, Littlewood and Polymath in Mathematics, Substance and Surmise: Views on the Meaning and Ontology of Mathematics, ed Ernest Davis, Philip J. Davis, Springer frames the polymath experiments in the context of G H Hardy's views of collaboration
 Martin, Ursula and Pease, Alison 2012 Seventy four minutes of mathematics: An analysis of the third MiniPolymath project Proceedings of AISB/IACAP 2012, 52105, is a preliminary study of the minipolymath experiments and provides a typology of the mathematical activities they exhibit  proof, examples, concept formation and the like.
 Martin, Ursula and Pease, Alison 2013 What does mathoverflow tell us about the production of mathematics? SOHUMAN workshop at CHI 2013, Paris is a preliminary study of the mathoverflow Q&A site for research mathematics, and provides a typology of questions and answers
 Martin, Ursula and Pease, Alison 2013 Mathematical practice, crowdsourcing, and social machines International Conference on Intelligent Computer Mathematics, Springer 7961, 98119 (invited plenary) lays out the research agenda in the context of formal proof and social machines
Modelling mathematical conversations with argumentation theory with Alison Pease and Joe Corneli Social machines provide models for mathematical argument using argumentation theory and LSC  the lightweight social calculus.
 Pease, Alison, Corneli, Joseph et al, 2017 Lakatosstyle collaborative mathematics through dialectical, structured and abstract argumentation Artificial Intelligence 246, 181–219
 Corneli, Joseph, Martin, Ursula, MurrayRust, Dave and Pease, Alison, 2017 Towards mathematical AI via a model of the content and process of mathematical question and answer dialogues , in Intelligent Computer Mathematics, 10th International Conference, Edinburgh, UK
 Corneli, Joseph; Martin, Ursula; MurrayRust, Dave; Pease, Alison; Puzio, Raymond; Nesin, Gabriela Rino, Modelling the way mathematics is actually done, FARM 2017  Proceedings of the 5th ACM SIGPLAN International Workshop on Functional Art, Music, Modeling, and Design, colocated with ICFP 2017
 Corneli, Joseph, Martin, Ursula, Nesin, Gabriela, and Pease, Alison 2017 Modelling mathematical conversations using inference anchoring theory, in preparation
Philosophy for mathematical practice with Andrew Aberdein, Alison Pease and Fenner Tanswell. We use the polymath online mathematical collaborations as an evidence base for understanding mathematical practice, in particular to assess notions of explanation in mathematics, with our most recent paper countering a number of assertions on explanation in the philosophical literature. Fenner Tanswell works on the connection between formal and informal proofs
 Tanswell, Fenner 2015 A Problem with the Dependence of Informal Proofs on Formal Proofs Philosophia Mathematica 23, 295310
 Tanswell, Fenner 2017 Conceptual engineering for mathematical concepts Inquiry, an interdisciplinary journal of philosophy, online first October 2017
 Aberdein, Andrew, Martin, Ursula and Pease, Alison, An empirical investigation into explanation in mathematical conversations, under review
The nature of mathematical collaboration, an ethnographic approach, with Lorenzo Lane.
 Lane, Lorenzo and Martin, Ursula 2015 Collaboration at the Isaac Newton Institute Report for the Isaac Newton Institute
 Lane, Lorenzo 2017 Fixed performances in fluid publics, 5th Innovation in Information Infrastructures (III) Workshop
 Lane, Lorenzo 2017 PhD thesis, University of Edinburgh
Mathematics policy and the impact of mathematics, with Laura Meagher. We use materials submitted for the 2014 Research Excellence Framework as an evidence base to assess the mechanisms by which mathematics has impact, highlighting the importance of interdisciplinarity, relationship building and the long term view.
 Meagher, Laura R. and Martin, Ursula, 2017 Slightly dirty maths: The richly textured mechanisms of impact Research Evaluation 26: 1527
 Popular accounts appeared in Times Higher, London Mathematical Society Newsletter, and Mathematics Today magazine, and the work was cited in a number of submissions to the 2017 HEFCE consultation on the REF.
The mathematics of Ada Lovelace, with Christopher Hollings and Adrian Rice In 2015 Ursula Martin organised Oxford's Ada Lovelace bicentenary celebrations, including collaborations with the Bodleian Library, BBC and various science museums. She curated an exhibition, now on display at the Silicon Valley Computer History Museum, and led the digitisation of Ada Lovelace's mathematics, with the support of the Clay Mathematics Institute. Numerous presentations included lectures at the Hay Festival, Computer History Museum and Gresham College.
 Hollings, Christopher; Martin, Ursula, and Rice, Adrian 2017 Ada Lovelace, a mathematical childhood, Journal of the British Society for the History of Mathematics 2: 221234 Covers Lovelace's education before 1840, which encompassed older traditions of practical geometry, newer textbooks influenced by continental approaches, wide reading, and a fascination with machinery, and challenges earlier judgements of her mathematical knowledge and skills which have impacted later scholarly and popular discourse.
 Hollings, Christopher; Martin, Ursula, and Rice, Adrian 2017 The LovelaceDe Morgan Mathematical Correspondence: A Critical ReAppraisal , Historia Mathematica 44: 202231 The first account by historians of mathematics of Lovelace's informal correspondence course with Augustus De Morgan. Detailed contextual analysis gives a corrected ordering of the archive material, and shows Lovelace learning good habits of study, a grounding in certain areas of higher mathematics, a critical attitude towards foundational principles, the ability to make perceptive mathematical observations, and exposure to ideas then current in British mathematical research. Contrary to earlier claims, Lovelace had the mathematical background for her famous 1843 paper, the potential for serious mathematical work.
 Hollings, Christopher; Martin, Ursula, and Rice, Adrian, 2018 Ada Lovelace: the making of a computer scientist , illustrated book to be published by the Bodleian Press
 Popular accounts have appeared in London Review of Books, BBC Oxford, EPSRC Blog, EDGE 2017 questions, London Mathematical Society Newsletter, Mathematics Today magazine, CORE magazine (Computer History Museum)
Earlier research
2003 onwards, compuational logic for control A totally novel “block diagram logic” was devised to solve a concrete problem raised by DSTL engineers, and then generalised to the abstract domain of traced monoidal categories. This showed that the new logic, and other results in computer science, are instantiations of this general concept; most strikingly Hoare’s logic of programs, devised in the 1960s, and the foundation of contemporary “industry standard” software verification. The paper received a “Best of 2013” award from the prestigious Computing Reviews journal. The pilot work was funded by QinetiQ, with subsquent funding from EPSRC.
 Arthan, Rob, Martin, Ursula and Oliva, Paulo 2013 A Hoare Logic for linear systems Formal Aspects of Computing, 25, 345363
 Arthan, Rob, Martin, Ursula, Mathiesen, Erik and Oliva, Paulo 2009 A general framework for sound and complete FloydHoare logics, ACM Trans on Computational Logic, 11, 112
 Boulton, Richard, Gottliebsen, Hanne, Hardy, Ruth, Kelsey, Tom and Martin, Ursula 2004 Design verification for control engineering, Integrated Formal Methods, Springer LNCS, 2999, 2135
1997 onwards, combining computational logic and computer algebra This was pioneering in developing new kinds of interface specifications for numerical libraries, which was extended to a new elegant solution to the problem of deficiencies in computer algebra systems, through using restricted calls to and from the Maple computer algebra system to specialist logic algorithms, via a limited interface that shields the user from complexity. The pilot work was developed during a sabbatical at SRI, and subsequently through a collaboration with NASA, with additional funding from EPSRC
 Gottliebsen, Hanne, Hardy, Ruth, Lightfoot Olga and Martin, Ursula 2013 Applications of real number theorem proving in PVS, Formal Aspects of Computing, 25, 9931016
 Gottliebsen, Hanne, Kelsey, Tom and Martin, Ursula 2005 Hidden verification for computational mathematics, Journal of Symbolic Computation, 39, 539567
 Dunstan, Martin, Kelsey, Tom, Martin, Ursula and Linton, Steve 1998 Lightweight formal methods for computer algebra, ACM Proceedings on Symbolic and Algebraic Computation, 1998, 8087
1990 onwards, Computer algebra and computational logic Early work included the first application of computational logic in group theory, obtaining results, at the time, well beyond the scope of standard techniques; novel unification algorithms inspired by group theory; and termination algorithms that provided a unified framework for understanding the diverse methods in use at the time.
 Martin, Ursula and Scott, Elizabeth 1997 The order types of termination orderings on monadic terms, strings and multisets, Journal of Symbolic Logic, 62, 624635
 Martin, Ursula and Lai, Mike 1992 Some experiments with a completion theorem prover, Journal of Symbolic Computation, 13, 81100
 Dick, Jeremy, Martin, Ursula and Kalmus, John 1990 Automating the KnuthBendix ordering, Acta Informatica, 28, 95119
 Martin, Ursula and Nipkow, Tobias 1989 Boolean Unification: the story so far, Journal of Symbolic Computation, 7, 275293
 Martin, Ursula 1989 A geometrical approach to multiset orderings, Journal of Theoretical Computer Science, 67, 3754
 Martin, Ursula and Nipkow, Tobias 1988 Unification in Boolean rings, Journal of Automated Reasoning, 4, 381396
1980 onwards, Group theory and combinatorics Research in group theory, combinatorics, and graph theory, mainly concerning symmetries of structures. First published paper, in 1980, provided a novel simple proof of a famous result of Gaschütz: in 2007, with Helleloid at Stanford, showed random groups of certain kinds have very restricted symmetry, a result with powerful implications which is still regularly applied in other domains.
 Helleloid, Geir and Martin, Ursula 2007 The automorphism group of a finite pgroup is almost always a pgroup, Journal of Algebra, 312, 294–329
 Martin, Ursula 1986 Almost all 𝑝groups have automorphism group a 𝑝group Bulletin of the American Mathematical Society, 15, 7882
 Webb, Ursula 1980 An elementary proof of Gaschütz' theorem Archiv der Mathematik 35 (1) 2326
Current research collaborators Andrew Aberdein, Joe Corneli, Chris Hollings, Lorenzo Lane, Laura Meagher, Alison Pease, Adrian Rice, Gabriela RinoNesin, Fenner Tanswell
Former RAs, graduate students and coauthors Andrew Adams, Rob Arthan, Richard Boulton, Muffy Calder, Adam Cichon, Dave Cohen, Victoria Coleman, Nick Cropper, Jeremy Dick, Martin Dunstan, Hanne Gottliebsen, Ruth Hardy, Geir Helleloid, John Kalmus, Tom Kelsey, Mike Lai, Olga Lightfoot, Steve Linton, Athen Ma, Erik Mathiesen, Natasa MilicFrayling, Bill Mitchell, Hanan Mohammed, Kathy Norrie, Tobias Nipkow, Paulo Oliva, Sam Owre, Peter Prohle, Liz Scott, Tim Storer, Duncan Shand, Phil Watson, Jeannette Wing.
Selected Publications

Modelling the Way Mathematics Is Actually Done
Joseph Corneli‚ Ursula Martin‚ Dave Murray−Rust‚ Alison Pease‚ Raymond Puzio and Gabriela Rino Nesin
2017.
Details about Modelling the Way Mathematics Is Actually Done  BibTeX data for Modelling the Way Mathematics Is Actually Done

The early mathematical education of Ada Lovelace
Christopher Hollings‚ Ursula Martin and Adrian Rice
In BSHM Bulletin: Journal of the British Society for the History of Mathematics. Pages 1–14. 2017.
Details about The early mathematical education of Ada Lovelace  BibTeX data for The early mathematical education of Ada Lovelace

The Lovelace–De Morgan mathematical correspondence: A critical re−appraisal
Christopher Hollings‚ Ursula Martin and Adrian Rice
In Historia Mathematica. 2017.
Details about The Lovelace–De Morgan mathematical correspondence: A critical re−appraisal  BibTeX data for The Lovelace–De Morgan mathematical correspondence: A critical re−appraisal