Skip to main content

The “Artificial Mathematician” Objection: Exploring the (Im)possibility of Automating Mathematical Understanding

  • Chapter
  • First Online:

Abstract

Reuben Hersh confided to us that, about forty years ago, the late Paul Cohen predicted to him that at some unspecified point in the future, mathematicians would be replaced by computers. Rather than focus on computers replacing mathematicians, however, our aim is to consider the (im)possibility of human mathematicians being joined by “artificial mathematicians” in the proving practice—not just as a method of inquiry but as a fellow inquirer.

This is a preview of subscription content, log in via an institution.

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   119.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   159.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   159.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    See (Davis & Hersh, 1981)

  2. 2.

    Almost verbatim quote from Bonsall (1982, p. 13)

  3. 3.

    There are exceptions. Consider the pons asinorum proof found by Gelernter’s program, which showed that the angles of an isosceles triangle are equal by noting that triangle ABC is congruent to triangle ACB (i.e., its mirror image) (Hofstadter 1999). While it can certainly be called an ingenuous move, that appreciation is not shared by the program itself and did not play a role in its reasoning or discovery.

  4. 4.

    Loosely adapted from (Hofstadter 1981/1985, p. 76–77)

  5. 5.

    Loosely adapted from a quote in (Hofstadter 1981/1985, p. 75)

  6. 6.

    Adapted from a quote by Wittgenstein in (Avigad 2008, p. 330–331)

  7. 7.

    By defining understanding by its constitution (physical or mental) or by an undefined wonder property, one could sideline all entities one isn’t keen to attribute understanding to (e.g., computers, other ethnicities, genders, or species) by marking out an inevitable difference in constitution or by simply denying the property (e.g., “humans can grasp meaning, computers can only pretend to” or “humans are conscious, but an artificial replication would be a zombie”) without specifying what makes the difference relevant. Such implicit chauvinism is much harder to substantiate if one must mark a difference in mathematically valuable performance. While still possible to deny certain performances the “mathematically valuable” attribute for chauvinistic reasons, one will be faced with the more demanding task of convincing a mathematical community which performances to (not) value.

  8. 8.

    Vervloesem (2010) even argues that conceptual shortcomings could be the main reason why computer proofs are still only on the fringe of mathematical practice. Enriching this aspect would lead to increasingly interesting (and more easily readable) proofs.

  9. 9.

    Adapted from a quote in (Hofstadter 1982, p. 15)

  10. 10.

    Dennett’s (1986/1998) metaphor

  11. 11.

    This section is loosely based on Dennett’s (2013) thought-experiment “Who is the author of Spamlet?” The mathematics is purely fictional.

References

  • Aberdein, A. (2006). Managing informal mathematical knowledge: techniques from informal logic. In Borwein, J.M. & Farmer, W.M. (Eds.), Mathematical Knowledge Management, (pp. 208–221). Berlin: Springer.

    Google Scholar 

  • Aberdein, A. (2007). The informal logic of mathematical proof. In Van Kerkhove B., Van Bendegem J.P. (eds) Perspectives on Mathematical Practices, (pp. 135–151). Dordrecht: Springer.

    Google Scholar 

  • Allo, P., Van Bendegem, J. P., Van Kerkhove, B. (2013). Mathematical arguments and distributed Knowledge. In A. Aberdein & I.J. Dove (Eds.), The argument of Mathematics, (pp. 339–360). New York: Springer.

    Google Scholar 

  • Avigad, J. (2008). Understanding proof. In Mancosu, P. (Ed.), The Philosophy of Mathematical Practice, (pp. 317–353). New York: Oxford.

    Chapter  Google Scholar 

  • Azzouni, J. (2004). The derivation-indicator view of mathematical practice. Philosophia Mathematica, 12(2), 81–106.

    Article  MATH  MathSciNet  Google Scholar 

  • Baker, A. (2015). Non-deductive methods in mathematics. In E. N. Zalta (Ed.), The Stanford Encyclopedia of Philosophy (Fall 2015 Edition). Retrieved from http://plato.stanford.edu/archives/fall2015/entries/mathematics-nondeductive

  • Benzmüller, C., Jamnik, M., Kerber, M., & Sorge, V. (1999). Agent based mathematical reasoning. Electronic Notes in Theoretical Computer Science, 3(23), 340–351.

    Article  MATH  Google Scholar 

  • Benzmüller, C., Kerber, M., Jamnik, M., & Sorge, V. (2001). Experiments with an agent-oriented reasoning system. In Baader F., Brewka G., Eiter T. (Eds.), KI 2001: LNAI 20174, (pp. 409–424). Berlin: Springer.

    Google Scholar 

  • Bonsall, F. F. (1982). A down-to-earth view of mathematics. The American Mathematical Monthly, 89(1), 8–15.

    Article  MATH  MathSciNet  Google Scholar 

  • Burge, T. (1998). Computer proof, a priori knowledge, and other minds. Philosophical Perspectives 12, 1–37.

    MATH  MathSciNet  Google Scholar 

  • Cellucci, C. (2000). The growth of mathematical knowledge: an open world view. In E. Grosholz & H. Breger (Eds.), The Growth of Mathematical Knowledge, (pp. 153–176). Dordrecht: Kluwer.

    Google Scholar 

  • Chalmers, D. J. (1990). Computing the thinkable. Behavioral and Brain Sciences, 13(04), 658–659.

    Article  Google Scholar 

  • Colton, S., Bundy, A., & Walsh, T. (1999). HR: Automatic concept formation in pure mathematics. In T. Dean (Ed.), Proceedings of the 16th International Joint Conference on Artificial Intelligence, (pp. 786–791). San Francisco: Morgan Kaufmann Publishers.

    Google Scholar 

  • Colton, S., Bundy, A., et al. (2000). Agent based cooperative theory formation in pure mathematics. In G. Wiggins (Ed.), Proceedings of AISB 2000 Symposium on Creative and Cultural Aspects and Applications of AI and Cognitive Science, (pp. 11–18). Birmingham, UK.

    Google Scholar 

  • Dennett, D.C. (1998). The Logical Geography of Computational Approaches: A View from the East Pole. In D.C. Dennett (Ed.), Brainchildren: Essays on designing minds (pp. 215–234). London: Penguin Books. (Original work published 1986).

    Google Scholar 

  • Davis, P. J., & Hersh, R. (1981). The mathematical experience. Boston: Houghton Mifflin.

    MATH  Google Scholar 

  • Dawson, J. W. (2006). Why do mathematicians re-prove theorems?. Philosophia Mathematica, 14(3) 269–286.

    Article  MATH  MathSciNet  Google Scholar 

  • Dennett, D.C. (2013). Intuition pumps and other tools for thinking. London: Penguin Books.

    Google Scholar 

  • Detlefsen, M. & Luker, M. (1980). The four-color theorem and mathematical proof. The Journal of Philosophy, 77(12), 803–820.

    Article  Google Scholar 

  • Forrest, S. (1990). Emergent computation: self-organizing, collective, and cooperative phenomena in natural and artificial computing networks. In S. Forrest (Ed.), Emergent computation. Cambridge, MA: MIT Press.

    Google Scholar 

  • Geist, C., Löwe, B., Van Kerkhove, B. (2010). Peer review and knowledge by testimony in mathematics. In B. Löwe and T. Müller (Eds.), Philosophy of Mathematics: Sociological Aspects and Mathematical Practice, (pp.155–178). London: College Publications.

    Google Scholar 

  • Van Bendegem, J. (1989). Foundations of mathematics or mathematical practice: is one forced to choose?. Philosophica, 43, 197–213.

    MathSciNet  Google Scholar 

  • Vervloesem, K. (2007). Computerbewijzen in de wiskundige praktijk. (MA Thesis, Katholieke Universiteit Leuven).

    Google Scholar 

  • Vervloesem, K. (2010). Mathematical concepts in computer proofs. In: Van Kerkhove, B., De Vuyst, J. & Van Bendegem, J.P. (Eds.), Philosophical Perspectives on Mathematical Practice, (pp. 61–87). London: College Publications.

    Google Scholar 

  • Hales, T. (2008). Formal proof. Notices of the AMS, 55(11), 1370–1380.

    MATH  MathSciNet  Google Scholar 

  • Harrison, J. (2008). Formal proof - Theory and Practice. Notices of the AMS, 55(11), 1395–1460.

    MATH  MathSciNet  Google Scholar 

  • Haugeland, J. (1979). Understanding natural language. The Journal of Philosophy, 76, 619–632.

    Article  Google Scholar 

  • Hersh, R. (1991). Mathematics has a front and a back. Synthese, 88(2), 127–133.

    Article  MATH  MathSciNet  Google Scholar 

  • Hofstadter, D.R. (1985). The Turing test: a coffeehouse conversation. In D. C. Dennett & D. R. Hofstadter (Eds.), The Mind's I: Fantasies and Reflections on Self and Soul, (pp. 53–67). Middlesex, England: Penguin Books. (Original work published 1981).

    Google Scholar 

  • Hofstadter, D. R. (1982). Artificial intelligence: Subcognition as computation. Indiana University Computer Science Department Technical Report No. 132.

    Google Scholar 

  • Hofstadter, D. R. (1999). Gödel, Escher, Bach: an eternal golden braid. New York: Basic Books.

    MATH  Google Scholar 

  • Lakatos, I. (1976). Proofs and refutations: the logic of mathematical discovery. Cambridge: University Press.

    Book  MATH  Google Scholar 

  • Lakoff, G., & Núñez, R. E. (2000). Where mathematics comes from: How the embodied mind brings mathematics into being. Basic books.

    Google Scholar 

  • Larson, C. E. (2005). A survey of research in automated mathematical conjecture-making. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 69, 297–318.

    Article  MATH  MathSciNet  Google Scholar 

  • MacKenzie, D. (1999) Slaying the Kraken: the sociohistory of a mathematical proof. Social Studies of Science, 29(1) 7–60.

    Article  MathSciNet  Google Scholar 

  • Mitchell, M., & Hofstadter, D. R. (1990). The emergence of understanding in a computer model of concepts and analogy-making. Physica D: Nonlinear Phenomena, 42(1–3), 322–334.

    Article  Google Scholar 

  • Pease, A. (2007). A computational model of Lakatos-style reasoning. (Doctoral dissertation, University of Edinburgh).

    Google Scholar 

  • Pease, A., Crook, P., Smaill, A., et al (2009). Towards a computational model of embodied mathematical language. Proceedings of AISB '09 Second Symposium on Computing and Philosophy.

    Google Scholar 

  • Pease, A., Smaill, A., Colton, S., et al (2010). Applying Lakatos-style reasoning to AI problems. In (J. Vallverdú (Ed.), Thinking Machines and the Philosophy of Computer Science: Concepts and Principles, (pp. 149–174). Hershey: IGI Global.

    Chapter  Google Scholar 

  • Rav, Y. (1999). Why do we prove theorems?. Philosophia Mathematica, 7(3) 5–41.

    Article  MATH  MathSciNet  Google Scholar 

  • Swart, E. (1980). The philosophical implications of the four-color problem. The American Mathematical Monthly, 87(9) 697–707.

    Article  MATH  MathSciNet  Google Scholar 

  • Steen, A., Wisniewski, M., & Benzmüller, C. (2016). Agent-based HOL reasoning. In International Congress on Mathematical Software, (pp. 75–81). Springer International Publishing.

    Google Scholar 

  • Tanswell, F. S. (2017). Proof, rigour and informality: a virtue account of mathematical knowledge (Doctoral dissertation, University of St Andrews).

    Google Scholar 

  • Tall, D., & Vinner, S. (1981). Concept image and concept definition in mathematics with particular reference to limits and continuity. Educational Studies in Mathematics, 12(2), 151–169.

    Article  Google Scholar 

  • Thompson, P. (1998). The nature and role of intuition in mathematical epistemology. Philosophia, 26(3), 279–319.

    Article  Google Scholar 

  • Turing A. (1985). Computing machinery and intelligence. In D. C. Dennett & D. R. Hofstadter (Eds.), The Mind's I: Fantasies and Reflections on Self and Soul, (pp. 53–67). Middlesex: Penguin Books. (Original work published 1950).

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Bart Van Kerkhove .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Delarivière, S., Van Kerkhove, B. (2017). The “Artificial Mathematician” Objection: Exploring the (Im)possibility of Automating Mathematical Understanding. In: Sriraman, B. (eds) Humanizing Mathematics and its Philosophy. Birkhäuser, Cham. https://doi.org/10.1007/978-3-319-61231-7_16

Download citation

Publish with us

Policies and ethics