Futarchy for Math

Previously, I wrote about Vadim’s work towards a decentralized marketplace for formal theorems. Now, he’s announced that the code for this site has been made open-source! 🎉

In honor of this, and in keeping with some of my recent posts on futarchy, here are some thoughts on the potential synergies of these epistemic technologies.

Theorem marketplaces and the theory-building problem

In a footnote on my previous post, I alluded to how I thought that one challenge formal theorem bounties face has to do with “theory building”, (which is a term I took from this essay by W. T. Gowers, I encourage you all to read it).

To elaborate on this with a visual example, take a look at this diagram.

This graph (zoomable/clickable version here) is the dependency chart for the “Prime Number Theorem +” project, a multi-collaborator effort to formalize various versions of the prime number theorem in Lean. As should be clear from the picture, the vast majority of effort in this project is not to do with formalization of PNT itself from its direct dependencies. Rather, most of the work has to do with the formalization of those dependencies (and of the dependencies of the dependencies, et cetera).

The larger the theorem gets, the more multifarious the dependencies become. I would like to be able to show you the same chart for Kevin Buzzard’s project to formalize Fermat’s Last Theorem, but unfortunately it’s grown so large that it seems it’s been split up into multiple pages. The FLT project is a particularly interesting example because as Kevin has described, an important part of the work of that project was making choices about what proof approach to take - As I understand it, much mathematical research has been done on the ideas behind Wiles’ original proof, and there are now multiple versions of the FLT proof to choose from. For the sake of the FLT project’s success, it’s important to choose one that will be amenable to formalization.

The problem this poses to theorem marketplaces is: Given that so much of the work of formalizing a major theorem is nonproximate to the proof of the theorem itself, how can we ensure that those who complete that work are compensated in proportion to their contribution? Put another way, how can markets do the important work of planning out something like a dependency chart in advance, so that we can tell what low level work is really needed?

Futarchy to the rescue

The framing of “markets need to formulate a plan” suggests futarchy as an answer. And closer inspection suggests this could be a promising application for other reasons: The person or team most confident in a particular plan seems likely to be both the one(s) with the most expertise in the style of approach behind that plan, as well as the most holdings in shares that the plan will succeed. Thus, there is a built-in incentive mechanism for them to contribute work towards realizing that plan when the futarchy decides to use it. Many of the markets the futarchy makes will touch on related formal questions, and so there will likely be arbitrage opportunities to support the liquidity in these markets, and the formal verification procedure provides a consistent, uncontroversial resolution mechanism for all of these.

A Proposal

Here is a proposal. Effectively, you could think of this as parametrizable pseudocode for a futarchic smart contract designed to maximize the likelihood of creating a successful formal proof of a target theorem by a target date.

1. We start with the theorem to be proved by year XXXX (for example “Fermat’s Last Theorem will be formally proved by 2029”).

2. Some percentage of the funding is set aside as a prize for the formalization itself.

3. The rest is used for the recursive construction of markets for intermediate results.

4. People can then propose candidates for what these results will be in the form of “factorizations”: Pairs or sets of subclaims that together imply the result (for example: “the Taniyama-Shimura conjecture is true” and “Taniyama-Shimura conjecture implies Fermat’s last theorem”). The important considerations for the subclaims are that they:

   1. Are likely to be proved by year XXXX (as the recursively constructed futarchic contract will attempt to make true).

   2. Together, they constitute formal proof of the main theorem (as guaranteed by the formal proof verification procedure).

5. If multiple factorizations are proposed, Futarchy decides which factorization gets funded.

You could augment this in a few ways:

• Make additional markets about the length of the proofs, and motivate the futarchy to find a short one, so that the proof is more comprehensible.

• If you are interested in a proof without a particular preference over time frame, you could create multiple futarchies, and set up an agent to bet NO on near-term proofs which funds those futarchies with its profits.

I’m not sure I’d really advocate that anyone put this into practice - I still think theorem marketplaces have the sociological problems I discussed before. Still, I think this is an interesting thought experiment on how mechanized mathematics can be tilted towards theory-building.