Research in metamathematics

Together with my student Torstein Vik I am working on a new conceptual framework for thinking about higher mathematics (or “real mathematics”, in the sense of Corfield). The starting point for this project is the observation that current attempts towards mathematical AI do not produce anything even remotely similar to the kind of research mathematics routinely produced by humans. We believe that by paying careful attention to (1) the ways humans do mathematics, and (2) the peculiarities of the human cognitive faculties, it is possible to create a new paradigm for modelling mathematical creativity that allows for interesting applications both in mathematical AI and in curriculum design for math courses at all levels.

Standard foundations for mathematics (expressed in terms of logics, set theory and type theory) leave no room for “soft” aspects of mathematics, like stories, analogies, and the many subtle relations between mathematical structures and human cognition. To model all of these, we need to look beyond conventional, “foundationalist” approaches to talking about mathematics. The new paradigm we are developing is called the MAD framework, where MAD is an acronym for three of the key components.

M for Machines: Iain McGilchrist has argued that there are no Things in the universe, only Processes. Insight from category theory and from the theory of computation suggests that functions (and more generally morphisms and functors) are more fundamental than sets (objects). We use the word machine as an umbrella term for all sorts of processes, functions, functors, etc, and think of these machines as our fundamental building blocks.

A for Analogies. In some of the ancient Vedic schools of philosophy, analogy is explicitly listed among the valid sources of knowledge. Douglas Hofstadter has for decades pushed the idea that analogy is the essence of human intelligence (Stanford report: “(almost) the whole enchilada”). In many top-level research papers, analogies play a prominent role (see for example Scholze’s ICM report, which has 21 mentions of analogy and similar words). However, the concept of analogy has no place in current formal models of mathematics. For example, there is no mechanism for witnessing or discovering analogies in the Lean language. We seek to incorporate analogies in our model, and argue that many analogies are faithfully encoded in the patterns made up by relevant machines.

D for Dialectics. Barry Mazur and many others have written on the role of stories in mathematics. The view of mathematics as a dialectical structure goes back at least to Albert Lautmann in the 30s. We develop a battery of structured questions which serves as a skeleton for the body of stories essential to a deep, “phenomenological”, understanding of mathematics. This dialectical structure weaves machines, analogies, and mathematical objects of all kinds into a landscape presented in a form that is adapted to the human cognitive facilities. The questions are somewhat reminiscent of Polya’s questions, except that we focus on mathematical theory-building rather than problem-solving.

A first report on MAD will appear soon, together with applications both in curriculum design and in attempts towards research-level mathematical AI.

Here are two conference articles and a couple of presentations from 2016/2017 which contain some embryos of our current work: