The Social Machine of Mathematics
Ursula Martin – University of Oxford
This project set out to investigate the phenomenon of mathematics as a social machine. I’ll give an overview of methodology, results and new questions. I’ll present the results of highly interdisciplinary work, using philosophy, social scence and history alongside computer science research in artificial intelligence, argumentation theory and verification, to show the scope for new 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. I’ll also look at how mathematics has impact, highlighting social factors and the importance of mathematics as part of human “cultural capital”.
Automated Reasoning in the Age of the Internet
Alan Bundy – University of Edinburgh
The internet hosts a vast store of information that we cannot and should not ignore. It’s not enough just to retrieve facts, to make full use of the internet we must also infer new information from old. This is an exciting new opportunity for automated reasoning, but it also presents new kinds of research challenge. There are a huge number of potential axioms from which to infer new theorems. Methods of choosing appropriate axioms are needed. Information is stored on the internet in diverse forms, and must be curated into a common format before we can apply inference to it. Some of the information is in a depleted state, e.g., RDF triples, and needs to be augmented with additional information, such as time, units, etc. We can employ forms of inference that are novel in automated reasoning, such as using regression to form new functions from sets of number pairs, and then extrapolation to predict new pairs. Information is of mixed quality and accuracy, so introduces uncertainty into the theorems inferred. Some inference methods, such as regression, also introduce uncertainty. Uncertainty estimates need to be inherited during inference and reported to users in an intelligible form.
We will report on Kobby Nuamah’s RIF system that explores this new research direction.
Redefining Mathematical Revolutions
Andrew Aberdein – Florida Intitute of Technology
In their account of theory change in logic, Aberdein and Read distinguish `glorious’ from `inglorious’ revolutions—only the former preserves all `the key components of a theory’ . A widespread view, expressed in these terms, is that empirical science characteristically exhibits inglorious revolutions but that revolutions in mathematics are at most glorious . Here are three possible responses:
0. Accept that empirical science and mathematics are methodologically discontinuous;
1. Argue that mathematics can exhibit inglorious revolutions;
2. Deny that inglorious revolutions are characteristic of science.
Where Aberdein and Read take option 1, option 2 is preferred by Mizrahi . This paper seeks to resolve this disagreement through consideration of some putative mathematical revolutions.
 Andrew Aberdein and Stephen Read, The philosophy of alternative logics, The Development of Modern Logic (Leila Haaparanta, ed.), Oxford University Press, Oxford, 2009, pp. 613–723.
 Donald Gillies (ed.), Revolutions in Mathematics, Oxford University Press, Oxford, 1992.
 Moti Mizrahi, Kuhn’s incommensurability thesis: What’s the argument?, Social Epistemology 29 (2015), no. 4, 361–378.
Abstract Relations: Media, Social Structure, and Sociable Structuralism in Modern Distributed Mathematics
Michael Barany – Dartmouth College, USA
In the late nineteenth and early twentieth century, systematic scientific abstracting played a crucial role in reconfiguring the sciences on an international scale. Beginning in the 1930s and accelerating with the 1940 launch of the American journal Mathematical Reviews, such abstracting activities helped to create a fundamental transformation, I shall argue, not just to the geographic scale of professional mathematics but to the very nature of mathematicians’ research and theories. It was not an accident that mathematical abstracting in this period coincided with an embrace across mathematical research fields of a distinctive form of symbolic and conceptual abstraction. Using archival sources and information from the online databases of Mathematical Reviews (MathSciNet) and the Zentralblatt für Mathematik (zbMATH), I shall examine the conjoined embodied and conceptual bases of mathematical abstracting and abstraction in the 1940s and 1950s, placing them in historical context within the first half of the twentieth century and then examining their consequences and legacies for the second half of the twentieth and early twenty-first century mathematics. Focused on scale, media, and the relationship between mathematical knowledge and its forms of articulation, my analysis will connect the changing social structure of modern mathematical research communities to their changing domains of investigation and resources for representation and consensus-making. To understand the challenges and opportunities of recent digital technologies and their associated communicative norms in mathematics, one must situate them in a century-long realignment of mathematical theory and practice.
Intelligent machinery via social machines: a proposal
Joseph Corneli – University of Edinburgh
I will give a sketch of a project at the nexus of social machines and artificial intelligence. The essence of the proposal is to build a computable model of both the technical content that users contribute to the popular Stack Exchange website, and the epistemic process of learning through Q&A. Agents will build a progressively improved model of the programming and mathematics domains, and fulfil Turing’s prophecy that future machines would be able to sharpen their wits by talking to each other.
Progress so far revolves around building a modelling language for mathematical communication and a process model of the behaviour that takes place in mathematical dialogues. The modelling language helps us make sense of the “kinematics” of mathematics (what people say) and the process model helps us understand the “dynamics” (why they say what they say). I will describe a worked example along these lines, and say some words about a preliminary implementation effort.
Modelling Arguments about Foundations of Mathematics in Structured Argumentation Theory
Marcos Cramer – University of Luxembourg, Luxembourg
Structured argumentation theory allows for a fine-grained model of argumentation and argumentative reasoning based on a formal language in which arguments and counterarguments can be constructed. In this talk we show preliminary results on the applicability of structured argumentation theory to argumentation about the foundations of mathematics.
The work presented in this talk is based on the ASPIC+ framework for structured argumentation (see ), in which one specifies strict and defeasible rules, from which arguments and an attack relation between arguments and their counter-arguments are defined. The distinction between strict and defeasible rules amounts to the difference between deductively valid modes of inference (e.g. conjunction introduction), and defeasible principles that generally hold but allow for exception (e.g. that dogs generally have four legs). Arguments built only from strict rules cannot be attacked.
Mathematical practice usually does not take place in a formal language governed by a formal logic, but in natural language. One of the aims of defining a formal foundation of mathematics is to make explicit which rules of inference are deemed acceptable. All widely studied foundations of mathematics, no matter whether classical or constructive, are based on a monotonic logic, i.e. on a logic in which accepting new axioms can never lead to less results being derivable. This property of foundational theories conforms well with the observable fact that mathematicians almost never reject previously established results, and in the few cases where this has happened, the original proof is considered mistaken.
The philosophical debates surrounding the acceptability of various foundational theories, on the other hand, cannot be faithfully modelled in a monotonic logic, as novel philosophical arguments can undermine a previously widely held view. The non-monotonic formalisms of structured argumentation theory can account for these non-monotonic aspects of philosophical argumentation. However, the fact that ASPIC+ presupposes the set of strict rules to be fixed and not up for debate makes it impossible to use ASPIC+ for modelling debates about which inferences are deductively valid, which has been a point of contention in the debates about the foundations of mathematics.
In a recent paper , we have proposed the ASPIC-END framework, a modification of the ASPIC+ framework that, besides other features, allows for debates about the correct rules of deductive inferences to be formally modelled. ASPIC-END replaces the strict rules of ASPIC+ by intuitively strict rules, which formalize the prima facie laws of logic which we pre-theoretically consider to be valid without exceptions, but which can nevertheless be given up after more careful examination. Unlike the strict rules of ASPIC+, an intuitively strict rule can be attacked by another argument, but unlike for a defeasible rule, the conclusion of an intuitive strict rule cannot be rejected if both the antecedent of the rule and the rule itself is accepted.
In this talk I will present ASPIC-END and illustrate on a simple example how it can be employed to formally model argumentation about the foundations of mathematics.
-  Jérémie Dauphin and Marcos Cramer. ASPIC-END: Structured Argumentation with Explanations and Natural Deduction. In Proceedings of the 2017 International Workshop on Theory and Applications of Formal Argumention (TAFA), 2017.
-  Sanjay Modgil and Henry Prakken. The ASPIC+ framework for structured argumentation: a tutorial. Argument & Computation, 5(1):31–62, 2014.
CrowdMath: Massive Research Collaboration among High School and College Students
Slava Gerovitch, Julia Braverman, and Anna Mirny – MIT
CrowdMath (http://artofproblemsolving.com/polymath/) is a free, massively collaborative mathematical research program open to high school and college students around the world. Inspired by Polymath projects, CrowdMath was established in 2016 as a joint effort by MIT PRIMES (Program for Research in Mathematics, Engineering and Science for High School Students) and the Art of Problem Solving. One year-long CrowdMath project was run in 2016, and two projects are underway in 2017. So far three research papers have been collectively authored by CrowdMath and posted on arXiv.org.
CrowdMath challenges the traditional modes of mathematical research in several key aspects: individual/joint vs open/massive; face-to-face vs virtual mentorship/advising; personal vs collective credit; and professional mathematicians vs students as participants.
This study is focusing on the CrowdMath culture from social and educational perspectives exploring the experiences of project participants and mentors. The data includes personal interviews and open-ended questionnaires administered online to groups of participants and mentors, as well as forum discussion records and foundational documents. Using integrative content analysis, we focus on such themes as the choice of research problems, motivation for participation, collective authorship, and the dynamics of online research collaboration and learning among high school and college students.
(I should mention that I’m program director of MIT PRIMES and one of the organizers of CrowdMath. We view PRIMES in general and CrowdMath in particular as a laboratory for trying experimental formats of research and learning. We are conducting this study in order both to improve the program and, more generally, to deepen our understanding of the culture of massive research collaboration in the digital age.)
Connecting two different views of mathematical explanation
Gila Hanna – Ontario Institute for Studies in Education, University of Toronto
I explore a connection between two distinct ways of defining mathematical explanation and thus of identifying explanatory proofs. The first definition is that current among philosophers of mathematics such as Kitcher (1981, 1989), Steiner (1978), and Lange (2014), in which a proof is considered explanatory when it helps account for a mathematical fact by clarifying how it is related to other such facts or why it follows from them. Such an explanatory proof is concerned with intra-mathematical factors and is not designed with any specific audience in mind, except for practicing mathematicians. This view has been designated by Delarivière, Frans, and Van Kerkhove (2016) as “Ontic” and defined as follows: “Proof P of theorem t has explanatory value if and only if P itself is the explanans of t regardless of whether it gives understanding to any particular agent”.
The second definition of explanation is the one current among mathematics educators, who consider a proof to be explanatory when it helps convey mathematical insights to an audience in a manner that is pedagogically appropriate. The explanatory power of a proof thus depends not only on the proof itself but also on cognitive factors, such as the quality of instruction, the maturity of the learners, and their existing mathematical knowledge. This latter view has been designated by Delarivière, Frans, and Van Kerkhove (2017) as “Epistemic” and defined as: “Proof P of theorem t has explanatory value if and only if the explanans consists of arguments (in the broad sense) including P that grants understanding of t for a particular agent S.”
The two views of mathematical explanation are quite different. I will show, however, citing examples, that insights from explanatory proofs as defined by philosophers of mathematics (ontic proofs) can often be useful in creating explanatory proofs in the pedagogical sense (epistemic proofs), and thus add value to the mathematics curriculum.
Delarivière, S., Frans, J., & Van Kerkhove, B. (2017). Mathematical explanation: A contextual approach. J. Indian Counc. Philos. Res. Springer: Online first.
Kitcher, P. (1981). Explanatory unification. Philosophy of Science, 48, 507-531.
Kitcher, P. (1989). Explanatory unification and the causal structure of the world. In P. Kitcher, & W. Salmon, (Eds.), Scientific explanation (pp. 410–505). (Minnesota Studies in the Philosophy of Science, Volume XIII), Minneapolis: University of Minnesota Press
Lange, M. (2014). Aspects of mathematical explanation: Symmetry, unity, and salience. Philosophical Review, 123(4), 485-531.
Steiner, M. (1978). Mathematical explanation. Philosophical Studies, 34, 135–151.
Linked structures of collaboration
Nick de Hoog – University of Konstanz
In this talk I will examine the linked structures of mathematical collaboration. In particular two social relationships are under consideration: that of co-authorship and that of supervisor-student. Features of these role-dependent social networks are discussed. The products that are associated with these two social roles are then compared on basis of text-external and text-internal properties. On basis of the properties of such products, inferences can be made on global trends in mathematical research.
To illustrate how a data-driven approach may offer a supplement for the study of the plurality of mathematical practices, some national-specific stereotypes and cliches about mathematical activity are elaborated on and tested on their accuracy. For this purpose, comprehensive data-sets and a proof corpus extracted from articles on the arXiv will be used.
A Cognitive Account of Mathematical Explanation
Matthew Inglis- Loughborough University
Explanations are central to education. Teaching consists in large part of offering instructional explanations, and learner-generated self-explanations can develop learners’ understanding. Given the ubiquity of explanations in mathematics teaching and learning, it is very puzzling that philosophers disagree about what they are, and even about whether they exist (e.g., Zelcer, 2013). How is it possible that learners and teachers are apparently able to generate explanations without anyone knowing what they are? In this talk I argue that Wilkenfeld’s (2014) functional explanation approach – which defines explanations to be those things that, under the right circumstances, produce understanding – provides a helpful way forward. In particular, I suggest that integrating a functional explanation approach with a traditional model of cognitive architecture can account for most earlier characterisations of mathematical explanation, including those offered by Steiner (1978), Kitcher (1981) and Lange (2014). From this approach I derive various predictions about mathematical explanation that can be tested empirically.
Socialising Mathematical Social Machines: Exploring the Transformative Role of Web Technologies
Lorenzo Lane- University of Oxford
Mathematicians have readily adopted new digital infrastructures, utilising them to build communities of practice (on MathOverflow.net), share knowledge and pre-print publications (arxiv.org), and solve problems (on PolymathProjects.org). Social machines are thus becoming part of the mainstream of mathematical practice. The question is: to what extent are these technologies transforming the field of mathematics? By exploring the processes by which these socio-technical systems are socialised I wish to understand how the transformative potential of social machines are restricted by the dominant discourse of the field. I shall argue that although the rhetoric surrounding the development of social machines in mathematics concerns the democratisation of knowledge, open access and equality of opportunity, the values actually promoted by social machines are instead oriented towards replicating existing power structures within the mathematical community. The social machines that mathematicians have built are geared towards privileging the presentation of the self: maintaining hierarchy, enhancing status, reputation and visibility and demonstrating efficacy, competitiveness and productivity. The transformative potentials of web technologies thus are constrained by existing social structures of the communities within which they are assimilated.
Hungarian mathematical culture: different interests, common features
András Máté -Department of Logic, Eötvös Loránd University Budapest, http://phil.elte.hu/mate/
Mathematics became in Hungary a very successful field of research from the beginning of 20th century – without almost any antecedent. People worked successfully in classical analysis, set theory, mathematical logic, combinatorics and graph theory, probability theory etc., but they shared some common ideas and interests. In my opinion, mathematical culture consists of those factors. The paper gives a short overview on the beginnings and conditions of the flourishing period of Hungarian mathematics, and then investigates three factors in the work of some mathematicians (and people who were not mathematicians but who were influenced by and have influenced Hungarian mathematical culture). The factors are the following:
- Importance of the intuitive side of mathematical thinking – mathematics is not just a structure of deductions, mathematics is mainly discovery.
- Philosophical interests extending from the classical questions of the philosophy of mathematics (nature of mathematical objects, certainty in mathematics) to the general role of mathematics in human culture.
- Interests in the education of mathematics, with the common fundamental thesis that in the ideal case, the student discovers (old theorems of) mathematics in the same way as the working mathematician discovers new theorems. The people to be investigated are:
- György (Georg) Pólya (classical analysis + heuristics of mathematics)
- László Kalmár (mathematical logic, computer theory + fallibilist philosophy of mathematics +writings about the education of mathematics)
- Rózsa Péter (mathematical logic, recursion theory + popularization of mathematics via discoveryand game)
- Alfréd Rényi (probability theory, graph theory etc. + ‘fictionalist’ philosophy of mathematics +active support of the modernization of mathematical education (together with Kalmár))
- Tamás Varga (the key figure of ‘new math’ in Hungary); and two non-mathematicians:
- Árpád Szabó (history of Greek mathematics + the origin and role of deductive method)
- Imre Lakatos (philosophy of mathematics and science + method of proofs and refutations).
Towards an argumentative understanding of mathematical discourse
Dave Murray-Rust, Edinburgh College of Art, University of Edinburgh
I am interested in the ways that everyday, embodied practices translate into distributed, computationally mediated systems. This talk will start by covering some of this ground, in particular looking at how ideas of wayfaring and trail-making come through in “Social Machines” – the large distributed systems that form an increasingly weighty part of society. This leads on to an engagement with mathematics, and the first steps towards a model of mathematical discourse that might allow computational intelligence to follow along with mathematics as it happens online, and eventually to engage in interesting ways.
Empirical Studies of Online Mathematics
Alison Pease – Department of Computing, University of Dundee
Online mathematical activity provides a novel and rich source of data for empirical investigation of mathematical practice – for example the community question answering system MathOverflow contains nearly 70,000 mathematical conversations, and polymath collaborations provide transcripts of the process of discovering proofs. Our preliminary
investigations have demonstrated the importance of “soft” aspects such as analogy and creativity, alongside deduction and proof, in the production of mathematics, and have given us new ways to think about the roles of people and machines in creating new mathematical knowledge. We discuss our investigations into these resources,
focusing on ways in which explanation and examples are used by mathematicians in both proofs and other mathematical contexts.
To what extent are existing proof assistants suitable for teaching elementary logic to university students?
Chris Sangwin – School of Mathematics, University of Edinburgh
Henri Maurer – University of Edinburgh
Mathematics is taught to many non-specialist students in higher education, including calculus to engineers and statistics to a wide (and growing) range of students including social sciences. Classical formal logic is also taught widely, for example to computer science and philosophy students. Compared to research on the teaching of other service subjects, research investigating the teaching of logic is comparatively neglected.
For context, our research will start with a brief review of the nature of logic as taught in a first formal university course, focusing on the nature of the subject itself and a brief discussion of what “logic” means at this level. Our methodology will be a review of current teaching practice in university philosophy courses. Included in this review we will discuss any software currently used to teach formal logic, and any existing research on the effectiveness of computer support for the teaching of logic.
We will also undertake a review of the options available to teachers in selecting software to support the teaching of logic, and proof more generally, including a detailed discussion of general proof assistants, automatic proof generation software and proof checkers. Specifically we will contrast any general software (including mainstream software such as Coq) with software designed specifically for teaching logic.
Bringing together these two reviews will enable us to answer the following primary research question: to what extent are existing proof assistants suitable for teaching elementary logic to university students? In order to effectively answer this question we will carefully define “suitable”. This includes aspects such as honesty to the nature of the subject, user interface, and later applicability beyond the course being taught.
The outcome will be a clearer understanding of what is being taught, the tools used to teach logic at university and the relationship of these tools to professional research software.
Paper Folding as a Mathematical Culture
Colin J. Rittberg – VUB
Michael Friedman – Humboldt U Berlin
Fold a sheet of paper flat onto itself and open it up again. The crease in the paper is a straight line. Fold the paper again such that the crease is folded onto itself, then open the paper up again. The new crease forms a line perpendicular to the first. By folding paper we can construct lines in a controlled fashion, and this allows for a geometry by paper-folding. This geometry is surprisingly strong: it can double the cube and trisect angles.
Paper as a material tool plus the activity of folding enables a mathematical culture which has attracted the attention of thinkers about mathematics education, recreational and research mathematics. In this talk, I will argue that geometry by paper-folding is a material reasoning practice, controlled by the physical realities of paper-like material. This allows for easy participation in the practice because, as Sundara Row has put it, it is ‘not necessary to take any statement on trust’; one can always fold and convince one-self with little theoretical baggage.
The practice of framing mathematical papers: Training to write to convince
Henrik Kragh Sørensen – Section for History and Philosophy of Science, Department of Science Education, Copenhagen University, Denmark
Line Edslev Andersen – Centre for Logic and Philosophy of Science, Vrije Universiteit Brussel, Brussels, Belgium.
Mikkel Willum Johansen – Section for History and Philosophy of Science, Department of Science Education, Copenhagen University, Denmark
Creative mathematical research involves numerous processes, which are not completely separated, neither cognitively nor temporally. These include identifying the problem area and approach, narrowing in on the problem at hand, developing intuitions and proof ideas, sketching proofs and making them more elaborate, and writing the results and proofs up for publication.
Our interest lies in the latter of these processes, namely the preparation of mathematical insight for communication through publication. Our theses are 1) that, in this process, the author is guided by an intended skeptical reader in a way that shapes the character of mathematical knowledge, and 2) that the image of the intended skeptical reader is created through the author’s inculcation into the relevant mathematical community and is influenced by its values and contingencies.
In this paper, we report on a (novel) way of conducting empirical philosophy of mathematical practices: We have conducted email-based, semi-structured interviews with members of a collaborative, mathematical project. We have been allowed a peek into a mathematical collaboration between a young, brilliant PhD student (Adam) and his experienced supervisor (Thomas). During their extensive correspondence, a rough draft by Adam was developed into a publishable research article through processes of textual editing, creative research, and narrative contextualization.
Our interviews are based on philosophical analyses of various draft versions of their joint paper. These analyses are grounded in our past research into how mathematicians proceed when acting as reviewers of mathematical papers. Our interviews thus investigate that communicative process anew, aiming to balance the perspective of the reviewer with that of the author. In the interviews, we focus on different purposes the authors of the joint paper might have when making revisions to the paper, such as trying to convince the intended reader that a result or an argument is new, interesting, or correct. In the presentation, we focus on the purpose of convincing the reader that an argument is correct. From the analyses of Andersen (2017), we expect that authors will aim to provide sufficient contextual information and mathematical details to convince the intended reader (as represented by the reviewer) that 1) their general argument fits into the landscape of what the reviewer knows and 2) that the specific, novel arguments are correct. However, how authors actually manage to achieve these two objectives has still not been analyzed philosophically.
Our presentation will include 1) a discussion of the research methodology of email-interviews with mathematicians, and 2) preliminary philosophical analyses drawn from the interviews.
Andersen, Line Edslev (Jan. 2017). “Social epistemology and mathematical practice. Perspectives on dependence, peer review, and joint commitments”. PhD thesis. Aarhus: Centre for Science Studies, Department of Mathematics, Aarhus University.
Proof, Rigour and Mathematical Virtues
Fenner Tanswell- University of St Andrews
“In this talk I will be investigating the application of virtue epistemology to specifically mathematical knowledge. I shall argue the case that this provides us with the tools to account for informal proofs and the nature of rigour as they are found in mathematical practice, overcoming obstacles that rule out the opposing formalist-reductionist approach. Furthermore, virtue-theoretic terminology allows us to make sense of a great deal of other phenomena of mathematics in practice.
Mathematical discourse among set theorists on the relationship between derivations and proofs
Keith Weber – Graduate School of Education, Rutgers
In the philosophy of mathematical practice, a distinction is frequently drawn between derivations (syntactical objects in a formal logical theory) and proofs (the types of arguments labeled as proofs in normal mathematical discourse). An important topic of investigation is what relationship, if any, exists between derivations and proofs in mathematical practice.
The goal of this presentation is to study the relationship between derivations and proofs in contemporary axiomatic set theory. Set theory is an interesting domain to study because, in contrast with most areas of mathematical investigation, (at least many) practitioners of set theory profess a commitment to establish that each theorem can, in principle, be verified by a finite derivation in a formal system (in ZF or ZFC or a metatheory), usually using predicate calculus. Indeed, the restriction to finitistic proofs and predicate calculus places important restrictions and provides surprising affordances for what can and cannot be proven. I will discuss how the relationship between derivation and proof is discussed and reasoned about, both in canonical texts (e.g., Jech, 2003; Kunen, 1980) and, in keeping with the themes of this workshop, on MathOverflow. The goal of this presentation will not be to discuss the logical or philosophical relationship between semantics and truth or formal theories and metatheories. Instead, the goal here is to analyze how these ideas, and more importantly, if and when these ideas, are discussed, both in formal references are discussed.
I will then use these findings to consider Azzouni’s (2004) derivation-indicator view of mathematical practice, which asserts that proofs map to mechanically verifiable derivations in an axiomatic system (although the nature of such an axiomatic system is deliberately left ambiguous), and other philosophers’ objections to this position (e.g., Pelc, 2009; Rav, 1999, 2007; Tanswell, 2015). To avoid misinterpretation, I emphasize that set theorists’ practice cannot be used to support Azzouni’s position. Set theory differs from most other areas of mathematics so one should avoid generalizing the practices of set theorists to other mathematicians. However, I will suggest that set theorists’ practices can diffuse some common objections to the derivation-indicator position.
Azzouni, J. (2004). The derivation-indicator view of mathematical practice. Philosophia Mathematica, 12(2), 81-106.
Jech, T. (2003). Set theory. Springer Science & Business Media.
Kunen, K. (1980). Set theory, Studies in Logic and the Foundations of Mathematics.
Pelc, A. (2008). Why do we believe theorems?. Philosophia Mathematica, 17(1), 84-94.
Rav, Y. (1999). Why do we prove theorems?. Philosophia mathematica, 7(1), 5-41.
Rav, Y. (2007). A critique of a formalist-mechanist version of the justification of arguments in mathematicians’ proof practices. Philosophia Mathematica, 15(3), 291-320.
Tanswell, F. (2015). A problem with the dependence of informal proofs on formal proofs. Philosophia Mathematica, 23(3), 295-310.