## Professor Ursula Martin CBE FREng FRSE DSc

Ursula Martin retired in January 2023. She is Professor Emerita at the University of Edinburgh, Emeritus fellow at Wadham College Oxford, a Distinguished Honorary Fellow of the Department of Computer Science and Technology at the University of Cambridge, and a Visiting Professor in both the School of Mathematics of the University of St Andrews, and the Mathematical Institute of the University of Oxford.

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, and an Honorary Fellow of Royal Holloway University of London, She holds a PhD and MSc from the University of Warwick, and an MA and BA from the University of Cambridge.

From 2014 to 2023 she held a UKRI/EPSRC Established Career Fellowship, *"The social machine of mathematics",* initially as a member of the Computer Science Department and Mathematical Institute of the University of Oxford (2014 - 2018), and subsequently as a member of the School of Informatics of the University of Edinburgh (2018-2023).

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 (2003 - 2013). She was Vice-Principal for Science and Engineering (2005 - 2009), and Director of the impactQM project (2009-2012), an innovative knowledge transfer initiative which was a finalist in the Times Higher Education Awards. Her career was interrupted for two years by ill-health, and she is grateful to Queen Mary for their support during this time, which enabled her to re-orient her research to mitigate the long-term consequences of extended chemotherapy. She was a Professor at the University of St Andrews (1992 - 2002), where she was the second female professor in any discipline since its foundation in 1411, the first having been appointed in some fifty years before. Earlier she was at Royal Holloway University of London (1985 - 1992), appointed in 1990 the University of London's first female professor of computer science, and before that held appointments at Manchester; and Urbana Champaign.

Throughout her career she was involved in many activities for women in science, including: establishing the pioneering Women@CL project at the University of Cambridge; serving on the UK Royal Society's Diversity Committee and chairing ACM-W, the Committee on Women of the ACM; and leading research and outreach based on the mathematics of Ada Lovelace. Numerous national roles included the UK Defence Science Advisory Council, the 2001 and 2008 UK HEFCE Research Assessment Exercise Panels for Computer Science, and the UKRI'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, broadened to encompass wider social and cultural approaches to understanding the circulation and impact of foundational research in computer science and mathematics.

**EPSRC Fellowship, the Social Machine of Mathematics**

The purpose of this UKRI/EPSRC Fellowship, 2014 - 2023, was to investigate cultures of mathematics viewed as a so-called* "Social machine", *an over-arching framework for considering human-machine collaboration. The resulting highly interdisciplinary portfolio of work drew on philosophy, social science, ethnography and history, alongside computer science research in artificial intelligence, argumentation theory and verification.

A particular focus was career development for postdocs, whose destinations included: Joe Corneli (Oxford Brookes), David Dunning (University of Pennsylvania), Chris Hollings (University of Oxford), Lorenzo Lane (UK government), Lee Macdonald (Greenwich Observatory), Jess Meagher (Royal Collection Trust), Alison Pease (University of Dundee), Gabriela Rino-Nesin (University of Brighton), Brigitte Stenhouse (University of Toronto), Máté Szabó (University of Greenwich), Fenner Tanswell (Technische Universität Berlin), Jacob Ward (University of Maastricht).

A landmark event was * Big Proof *, a major programme at the Cambridge Newton Institute in Summer 2017, which is credited with shifting the dial on how mathematicians think about using computation in proof. Other workshops included:

*7-8 April 2017, Oxford Mathematics;*

**Group knowledge and mathematical collaboration***5-7 December 2017, Oxford Mathematics;*

**Enabling mathematical cultures***Mathematical Collaboration II*St Andrews 7-8 April 2018, and

*27-31 May 2019, ICMS Edinburgh.*

**Big Proof II**### EPSRC Fellowship: Impact

* Mathematics policy and the impact of mathematics* 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. The work was cited in a number of submissions to the 2017 HEFCE consultation on the REF, and in the 2019 Bond Review on Mathematics Knowledge Transfer, which led a substantial uplift in UK mathematics funding.

**Meagher,****Laura R.**and Martin, Ursula, 2017**Slightly dirty maths: The richly textured mechanisms of impact****Research Evaluation 26 (15-27)**- Widely disseminated through invited pieces in Times Higher, London Mathematical Society Newsletter, and IMA Mathematics Today magazine.

* Collaborations with Libraries and Museums* led to four public engagement projects, and a UKRI Impact Case Study, as described at the links:

**The mathematics of Ada Lovelace, 2015-2021**, including a popular book, highly cited journal papers, museum displays in the UK and USA, a conference, numerous public talks, and collaborations with composers. The work was submitted as an Impact Case Study for the 2021 UK Research Excellence Framework.**Oxford's female computing pioneers, 2020**, a series of oral history interviews by Georgina Ferry, archived in Oxford's Bodleian Library.**Imagining AI, 2022**, including a workshop, displays at the Bodleian Library and the History of Science Museum, and bespoke video of the Jevons "Reasoning piano". A much larger display had originally been planned, but could not go ahead because of the pandemic.**Archiving Babbage 2022**, the cataloguing, digitisation and dissemination of MSS Buxton, manuscripts of Charles Babbage collected by Harry Wilmot Buxton and now held in Oxford's History of Science Museum.

### EPSRC Fellowship: Main research themes

* Mathematical collaboration online O*nline collaboration captures informal processes that are normally not recorded. A variety of quantitative and qualitative techniques were used to investigate the PolyMath projects, and the MathOverflow Q&A site,

*to understand what's involved in developing a proof, and the fit with the model provided by social machines.*

**Alison Pease, Ursula Martin, Fenner Stanley Tanswell, Andrew Aberdein 2020**,*Using crowdsourced mathematics to understand mathematical practice*ZDM 52, 1087-1098*A capstone article, by invitation for a special issue, presenting our methods in the context of mathematical education***Martin, Ursula 2016***Computational logic and the social*Journal of Logic and Computation, 26, 467-477*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, the major conference on automated deduction) looks at social machines in the context of formal proof and experimental mathematics***Martin, Ursula and Pease, Alison 2015,***Hardy, Littlewood and Polymath**in**frames the polymath experiments in the context of G H Hardy's views of collaboration***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, 98-119***(invited plenary) lays out the research agenda in the context of formal proof and social machines***Martin, Ursula and Pease, Alison 2012***Seventy four minutes of mathematics: An analysis of the third Mini-Polymath project***Proceedings of AISB/IACAP 2012, 52-105**,*is a preliminary study of the mini-polymath experiments and provides a typology of the mathematical activities they exhibit - proof, examples, concept formation and the like.*

* Modelling mathematical conversations with argumentation theoryy *Social machines provide models for mathematical argument using argumentation theory and LSC - the lightweight social calculus.

**Joseph Corneli, Ursula Martin, Dave Murray-Rust, Gabriela Rino-Nesin, Alison Pease 2019****Argumentation theory for mathematical argument****Argumentation 33, 173-21***A prototype system for modelling mathematical arguments using Reed's argumentation calculus and Robertson's LSC***Joseph Corneli, Simon Holland, Alison Pease et al 2018,***Patterns of design*Proceedings of the 23rd European Conference on Pattern Languages of Programs, 1-11**Pease, Alison,**Corneli, Joseph et al, 2017*Lakatos-style collaborative mathematics through dialectical, structured and abstract argumentation*Artificial Intelligence 246, 181–2192017**Corneli, Joseph,**Pease, Alison,**Martin, Ursula, Murray-Rust, Dave and***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; Murray-Rust, Dave; Pease, Alison; Puzio, Raymond; Nesin, Gabriela Rino, 2017***Modelling the way mathematics is actually done,*FARM 2017 - Proceedings of the 5th ACM SIGPLAN International Workshop on Functional Art, Music, Modeling, and Design, co-located with ICFP 2017

* Philosophy and mathematical practice *The "Polymath" online mathematical collaborations were used as an evidence base for understanding mathematical practice, in particular to assess notions of explanation in mathematics. Fenner Tanswell works on the connection between formal and informal proofs

**Alison Pease, Andrew Aberdein, Ursula Martin, 2019,***Explanation in mathematical conversations: An empirical investigation,*Philosophical Transactions of the Royal Society A 377*Uses analysis of a polymath conversation as an**evidence base to assess 9 hypotheses, drawn from the philosophical literature, about mathematical explanation***Lorenzo Lane, Ursula Martin et al, 2019,***Journeys in mathematical landscapes: genius or craft?*Proof Technology in Mathematics Research and Teaching (Springer) 197-212*Explores**craft as a metaphor for creating mathematics***Fenner Tanswell 2018***Conceptual engineering for mathematical concepts*Inquiry 61, 881-913**Fenner Tanswell 2017***Playing with LEGO® and Proving Theorems,*LEGO® and Philosophy: Constructing Reality Brick by Brick, 217-226**Fenner Tanswell 2016***Saving proof from paradox: Gödel’s paradox and the inconsistency of informal mathematics*, Logical Studies of Paraconsistent Reasoning in Science and Mathematics, 159-173**Fenner Tanswell 2015***A Problem with the Dependence of Informal Proofs on Formal Proofs*Philosophia Mathematica 23, 295-310

**The early roots of contemporary mathematical and computational practices **

**David Dunning, 2023,***George Boole and the ‘Pure Analysis’ of the Syllogism*. 2023*In*Aristotle’s Syllogism and the Creation of Modern Logic: Between Tradition and Innovation, FGHI–FKLI, eds. Lukas M. Verburgt and Matteo Cosci. Bloomsbury Academic.**David Dunning, 2021,***The Work of Writing Programs: Logic and Inscriptive Practice in the History of Computing*, IEEE Annals of the History of Computing 25, 27-42**David Dunning, 2021,***The Logician in the Archive: John Venn’s Diagrams and Victorian Historical Thinking*. Journal of the History of Ideas 82, 593-614**David Dunning, 2020,***Always Mixed Together’: Notation, Language, and the Pedagogy of Frege’s Begriffsschrift*. Modern Intellectual History 17 (1099-1131)**Máté Szabó et al (2023).***How Computers Entered the Classroom in Hungary: A Long Journey from the Late 1950s into the 1980s.*In Flury C, Geiss M (Ed.), How Computers Entered the Classroom, 1960–2000: Historical Perspectives. Oldenbourg:De Gruyter**Máté Szabó (2021).***Péter on Church’s Thesis,*17th Conference on Computability in Europe, CiE 2021, Springer (pp. 434-445).**Máté Szabó (2021).***From the West to the East and Back Again: Hungary's Early Years in the Ryad*. IEEE Xplore Digital Library,**Máté Szabó (2020).***Alonzo Church Tihanyban*. Érintö, Elektronikus Matematikai Lapok**Jacob Ward, 2020,***Computer Models and Thatcherist Futures: From Monopolies to Markets in British Telecommunications*, Technology and Culture 61 (843-870)

**T***h*e nature of mathematical collaboration, an ethnographic appro**ach**** **These *careful ethnographic studies at mathematics research institutes looked at the activities of mathematicians as they collaborated in person, and identified a variety of processes for generating shared knowledge *

**Lane, Lorenzo****2017***Fixed performances in fluid publics,*5th Innovation in Information Infrastructures (III) Workshop**Lane, Lorenzo and Martin, Ursula****2015***Collaboration at the Isaac Newton Institute*Report for the Isaac Newton Institute

### Research in verification, logic and algebra

** 2003 onwards, computational 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. Significant papers include:

**Arthan, Rob, Martin, Ursula and Oliva, Paulo 2013***A Hoare Logic for linear systems*Formal Aspects of Computing, 25, 345-363**Arthan, Rob, Martin, Ursula, Mathiesen, Erik and Oliva, Paulo 2009***A general framework for sound and complete Floyd-Hoare logics*, ACM Trans on Computational Logic, 11, 1-12**Boulton, Richard, Gottliebsen, Hanne, Hardy, Ruth, Kelsey, Tom and Martin, Ursula 2004***Design verification for control engineering*, Integrated Formal Methods, Springer LNCS, 2999, 21-35

* 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. Significant papers include:

**Gottliebsen, Hanne, Hardy, Ruth, Lightfoot Olga and Martin, Ursula 2013***Applications of real number theorem proving in PVS*, Formal Aspects of Computing, 25, 993-1016**Gottliebsen, Hanne, Kelsey, Tom and Martin, Ursula 2005***Hidden verification for computational mathematics*, Journal of Symbolic Computation, 39, 539-567**Dunstan, Martin, Kelsey, Tom, Martin, Ursula and Linton, Steve 1998***Lightweight formal methods for computer algebra*, ACM Proceedings on Symbolic and Algebraic Computation, 1998, 80-87

* 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. Significant papers include:

**Martin, Ursula and Scott, Elizabeth 1997***The order types of termination orderings on monadic terms, strings and multisets*, Journal of Symbolic Logic, 62, 624-635**Martin, Ursula and Lai, Mike 1992***Some experiments with a completion theorem prover*, Journal of Symbolic Computation, 13, 81-100**Dick, Jeremy, Martin, Ursula and Kalmus, John 1990***Automating the Knuth-Bendix ordering*, Acta Informatica, 28, 95-119**Martin, Ursula and Nipkow, Tobias 1989***Boolean Unification: the story so far*, Journal of Symbolic Computation, 7, 275-293**Martin, Ursula 1989***A geometrical approach to multiset orderings*, Journal of Theoretical Computer Science, 67, 37-54**Martin, Ursula and Nipkow, Tobias 1988***Unification in Boolean rings*, Journal of Automated Reasoning, 4, 381-396

* 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. Significant papers include:

**Helleloid, Geir and Martin, Ursula 2007***The automorphism group of a finite p-group is almost always a p-group*, Journal of Algebra, 312, 294–329**Martin, Ursula 1986***Almost all 𝑝-groups have automorphism group a 𝑝-group***Bulletin of the American Mathematical Society, 15, 78-82****Webb, Ursula 1980***An elementary proof of Gaschütz' theorem*Archiv der Mathematik 35 (1) 23-26

**Research assistants, graduate students and co-authors 1983-2023 ** Andrew Aberdein, Andrew Adams, Rob Arthan, Richard Boulton, Muffy Calder, Adam Cichon, Dave Cohen, Victoria Coleman, Joe Corneli, Nick Cropper, Jeremy Dick, David Dunning, Martin Dunstan, Hanne Gottliebsen, Ruth Hardy, Geir Helleloid, Chris Hollings, John Kalmus, Tom Kelsey, Mike Lai, Lorenzo Lane, Olga Lightfoot, Steve Linton, Athen Ma, Lee Macdonald, Erik Mathiesen, Laura Meagher, Natasa Milic-Frayling, Bill Mitchell, Hanan Mohammed, Dave Murray-Rust, Kathy Norrie, Tobias Nipkow, Paulo Oliva, Sam Owre, Alison Pease, Peter Prohle, Adrian Rice, Gabriela Rino-Nesin, Elizabeth Scott, Brigitte Stenhouse, Tim Storer, Duncan Shand, Máté Szabó, Fenner Tanswell, Jacob Ward, Phil Watson, Jeannette Wing.