Big Math and the One-Brain Barrier: 
A Position Paper and Architecture Proposal

Jacques Carette, William M. Farmer, Michael Kohlhase, and Florian Rabe

2019

Abstract

Over the last decades, a class of important mathematical results has
required an ever increasing amount of human effort to carry out. For
some, the help of computers is now indispensable.  We analyze the
implications of this trend towards big mathematics, its relation to
human cognition, and how machine support for big math can be
organized.

The central contribution of this position paper is an information
model for doing mathematics, which posits that humans very efficiently
integrate five aspects of mathematics: inference, computation,
tabulation, narration, and organization.  The challenge for
mathematical software systems is to integrate these five aspects in
the same way humans do.  We include a brief survey of the state of the
art from this perspective.