Introduction

In software design, several key principles share a common foundation: the concept of factoring, or breaking complex problems into smaller, manageable parts. Three prominent examples are:

Unix philosophy: Design programs to do one thing well.
Black box abstraction: Isolate functionality to focus on core problems.
Interface-based programming: Build systems from well-defined, interconnected modules.

These principles, though known by different names, all rely on factoring to create efficient, reliable, and maintainable systems. Even when developers aren't sure how to factor a problem, they often intuitively recognize that it should be factored: this notion of factoring has a fundamental role in effective software design.

In this post, we consider how this idea of factoring applies to mathematical theorem proving. Similar to the Unix philosophy, there is a sort of factoring that takes place in mathematics: breaking down difficult conjectures into simpler lemmas. But just as in software, collaboration is crucial for solving these problems, with mathematicians often building upon one another’s work, even without full awareness of all the details involved. This is reminiscent of Milton Friedman’s Lesson of the Pencil: the wood chopper on one side of the world has nothing in common with the granite miner on another, and neither of them know how to make a pencil by themselves. Yet, their incentives fall such that pencils get manufactured as a global project.

Just as in software and in the manufacturing of a pencil, success relies on collaboration and breaking problems into manageable parts. To that end, we present a first attempt at an incentive structure to encourage collaborative theorem proving, inspired by a recent concept called Plausible Fiction.

Plausible Fiction

In a recent Topos Institute blog post, Spivak proposed a general theory of change, which he called Plausible Fiction. A work of plausible fiction has four requirements:

It begins with the world as it is now, including all relevant details and without distortion;
It ends with a future that the author desires;
It follows a trajectory that obeys natural laws and social dynamics; and
It is memetically fit for collaborators: they readily understand and can spread the idea.

The mechanism that makes plausible fiction work is gap-filling. To collaborate on a work of plausible fiction, one finds a gap in the sto...

Posts

Wikitag Contributions

Comments