FairBot and Its Mirror:
An Open Problem in Open-Source Game Theory
Is a Proof-Length Problem

Daniel Kang†
August 2026
Abstract
Open Problem 3 of Critch, Dennis and Russell [1]A. Critch, M. Dennis, S. Russell, “Cooperative and Uncooperative Institution Designs: Surprises and Problems in Open-Source Game Theory,” arXiv:2208.07006. asks for the outcome of \(\mathrm{DUPOC}(k)\) against \(\mathrm{CUPOD}(k)\): two agents that read each other's source code and search for proofs of bounded length. We report four things. The two agents are the same program under relabelling of the two action tokens, which collapses the folklore puzzle about why the “nicer” agent defects against itself. The outcome is decided entirely by whether either bounded search succeeds, and any success forces a proof of bounded consistency of comparable length. In any formalisation where the relabelling is a symmetry of the proof system, the outcome is \((D,C)\) for every \(k\) — unconditionally, constructively, and machine-checked in Lean 4. In the standard arithmetisation the answer is \((D,C)\) if and only if consistency proofs are superlinear, which is an equivalence rather than a reduction. We also show that the framework's own axioms do not determine the answer: all three outcomes are realisable across sound proof systems. That too is machine-checked. Section 9 lists, in full, what remains assumed.

1 Introduction

If AI systems are going to negotiate with one another, they will do so under a condition that has no analogue between humans: they can read each other's source code. That single change dissolves most of the machinery of classical game theory, because a player's strategy is no longer a hidden intention but a published object that the opponent can reason about. Open-source game theory is the attempt to say what happens next.

The founding construction is Barasz et al.'s FairBot [2]M. Barasz, P. Christiano, B. Fallenstein, M. Herreshoff, P. LaVictoire, E. Yudkowsky, “Robust Cooperation in the Prisoner's Dilemma: Program Equilibrium via Provability Logic,” arXiv:1401.5577.: an agent that cooperates with \(O\) if and only if it can prove that \(O\) cooperates with it. Self-reference is handled by Kleene's recursion theorem, so the definition is not circular, and Löb's theorem then does something remarkable — it makes FairBot cooperate with itself, without ever being exploitable. Cooperation becomes a theorem rather than an equilibrium selection.

Critch, Dennis and Russell push the construction further and find that it stops being intuitive. Renaming FairBot to DUPOCDefect Unless Proof Of Cooperation: output \(C\) iff you can prove the opponent outputs \(C\)., they introduce its apparent mirror image, CUPODCooperate Unless Proof Of Defection: output \(D\) iff you can prove the opponent outputs \(D\)., which cooperates unless it can prove the opponent defects. CUPOD looks like the more generous agent. It defects against itself. DUPOC, the suspicious one, cooperates with itself. And the matchup between them is left open.

This post resolves that matchup in the cases where it can be resolved, identifies exactly what the remaining case is equivalent to, and machine-checks the parts that carry the argument. The short version is that the problem is not really about provability logic at all. Every sentence involved is decidable; there is no incompleteness anywhere in it. What is left, once the modal structure is stripped away, is a question about how many symbols it takes to write something down.

2 The Two Agents Are One Program

Write \(\Box_k\varphi\) for “there is a proof of \(\varphi\) of length at most \(k\)”, with \(k\) in binary, so that the agents' source codes and the sentences below have size \(O(\log k)\).

Statement 1 (One program, two tokens). PROVED
DUPOC and CUPOD are instances of a single parametrised program.
Proof. Define, for a token \(\alpha \in \{C,D\}\),
$$P_\alpha(O) \;=\; \begin{cases}\alpha & \text{if } \Box_k\bigl(O(P_\alpha)=\alpha\bigr)\\ \bar\alpha & \text{otherwise.}\end{cases}$$
Then \(P_C\) outputs \(C\) exactly when it can prove the opponent outputs \(C\), which is DUPOC; and \(P_D\) outputs \(D\) exactly when it can prove the opponent outputs \(D\), which is CUPOD. The two source codes are related by the relabelling \(C \leftrightarrow D\). □

This is a small observation with a large consequence, because it explains the result that made the pair interesting in the first place.

Statement 2 (Why the “nicer” agent defects). PROVED
The self-play theorems for DUPOC and CUPOD are one theorem, applied at two values of \(\alpha\).
Proof. Löb's theorem applied to \(P_\alpha\) against \(P_\alpha\) yields \(P_\alpha(P_\alpha)=\alpha\), and the argument does not mention which token \(\alpha\) is. Instantiating at \(\alpha=C\) gives mutual cooperation for DUPOC; at \(\alpha=D\), mutual defection for CUPOD. □
Remark. The usual intuition — that CUPOD cooperates only if there is no proof it will not, and one can never establish that no proof exists — is not the mechanism. The mechanism is that \(\alpha\) is a free parameter and Löb is blind to it. Löb's theorem awards each agent whatever it went looking for. DUPOC searches for cooperation and finds it; CUPOD searches for defection and finds it. Niceness is not the operative variable. The search target is.

3 Normal Form

Set \(X = \ulcorner P_D(P_C)=C\urcorner\) (“CUPOD cooperates with DUPOC”) and \(Y = \ulcorner P_C(P_D)=D\urcorner\) (“DUPOC defects against CUPOD”). Reading the source code off via the recursion theorem gives two equations, and these are the only facts about the agents used anywhere below:

$$\text{(E1)}\quad Y \leftrightarrow \neg\Box_k X, \qquad\qquad \text{(E2)}\quad X \leftrightarrow \neg\Box_k Y.$$

Write \(u := \Box_k X\) and \(v := \Box_k Y\). These are statements about a finite search, so each is simply true or false.

Statement 3 (Trichotomy). PROVED LEAN-CHECKED
The outcome is determined by which search succeeds, and at most one can.
ConditionMeaningOutcome
\(u\)DUPOC finds its proof\((C,C)\)
\(v\)CUPOD finds its proof\((D,D)\)
\(\neg u \wedge \neg v\)neither search succeeds\((D,C)\)
Proof. If \(u\) then \(X\) is true by soundness, so CUPOD cooperates; and by (E1) \(Y\) is false, so DUPOC cooperates. If \(v\), symmetrically, \((D,D)\). If neither, (E1) and (E2) make both \(X\) and \(Y\) true, so CUPOD cooperates and DUPOC defects. Finally \(u \wedge v\) is impossible: \(u\) gives \(X\) true, and (E2) then gives \(\neg v\). □
Statement 4 (No exploitation). PROVED LEAN-CHECKED
The fourth outcome \((C,D)\), in which DUPOC cooperates and CUPOD defects, cannot occur.
Proof. It would require \(\neg X \wedge \neg Y\); but \(\neg Y\) gives \(\Box_kX\) by (E1), and soundness then makes \(X\) true. □

So the conjectured answer \((D,C)\) is exactly the claim that both bounded searches come up empty. That is a statement about proof lengths, and no amount of modal reasoning can see it: the semantics of provability logic is blind to how long a proof is.

4 The Ex Falso Reduction

Let \(\mathrm{Con}_n\) abbreviate “there is no proof of \(\bot\) of length \(\le n\)”, and let \(s(n)\) denote the length of the shortest \(\mathrm{PA}\)-proof of \(\mathrm{Con}_n\).

Statement 5 (Ex Falso Reduction). PROVED
\(\mathrm{PA}\vdash_{O(\log k)} \neg\Box_kY \rightarrow \mathrm{Con}_{k-\lambda}\), where \(\lambda = |Y| + c = O(\log k)\).
Proof. Argue in \(\mathrm{PA}\). If \(p\) proves \(\bot\) with \(|p| \le k-\lambda\), append the ex falso step to \(Y\); the result proves \(Y\) with length \(\le |p| + |Y| + c \le k\), so \(\Box_kY\). Contrapose. The formalisation is one fixed constant-size lemma, \(\forall p\,\forall\psi\,\bigl(\mathrm{Prf}(p,\bot)\to\mathrm{Prf}(\mathrm{exf}(p,\psi),\psi) \wedge |\mathrm{exf}(p,\psi)| \le |p|+|\psi|+c\bigr)\), instantiated at \(\psi = Y\), which costs \(O(\log k)\). □

Applied to (E2), and symmetrically to (E1), this says that either search succeeding forces a cheap consistency proof:

$$u \;\Longrightarrow\; s\bigl(k-O(\log k)\bigr) \le k + O(\log k), \qquad v \;\Longrightarrow\; s\bigl(k-O(\log k)\bigr) \le k + O(\log k).$$
Statement 6 (Hard consistency forces \((D,C)\)). PROVED LEAN-CHECKED
If \(s(n) > n + \Theta(\log n)\) for all large \(n\), then \(\mathrm{outcome}(\mathrm{DUPOC}(k),\mathrm{CUPOD}(k)) = (D,C)\) for all large \(k\).
Proof. Immediate from Statement 5 and Statement 3. □
Caveat. The Lean development proves the logical step from the extraction and the hardness hypothesis. The extraction itself (Statement 5) is a syntactic fact about a concrete proof calculus and is not formalised. See Section 9.

5 The Mirror Theorem

Return to the relabelling \(\sigma : C \leftrightarrow D\) of Statement 1. On the two sentences it acts by

$$X = \ulcorner P_D(P_C)=C\urcorner \;\overset{\sigma}{\longmapsto}\; \ulcorner P_C(P_D)=D\urcorner = Y, \qquad Y \overset{\sigma}{\longmapsto} X,$$

and hence on outcomes by \((C,C) \leftrightarrow (D,D)\) with \((D,C)\) fixed. The conjectured answer is the symmetry-fixed outcome, and the other two are the symmetry-broken pair. That is the reason \((D,C)\) feels right, and it can be turned into a proof whenever the relabelling is a symmetry of the proof system rather than merely of the specification.

It costs nothing to arrange. Let \(\mathrm{PA}^{+}\) be \(\mathrm{PA}\) in the language with two fresh constants \(\mathsf c,\mathsf d\), axioms \(\mathrm{PA} \cup \{\mathsf c \ne \mathsf d,\ \mathsf d \ne \mathsf c\}\), under a numbering giving \(\mathsf c\) and \(\mathsf d\) codes of equal length; let the agents' actions be \(\mathsf c,\mathsf d\) and their proof search range over \(\mathrm{PA}^{+}\). This is a conservative extension of \(\mathrm{PA}\), and the agents are unchanged.

Statement 7 (Mirror Theorem). PROVED LEAN-CHECKED
In the token-symmetric formalisation, \(\mathrm{outcome}(\mathrm{DUPOC}(k),\mathrm{CUPOD}(k)) = (D,C)\) for every \(k\).
Proof. Three facts. (i) \(\sigma\) is a bijection on formulas preserving symbol count, maps the axiom set onto itself, and commutes with the inference rules; so \(\pi \mapsto \sigma(\pi)\) is a length-preserving bijection on proofs with \(\sigma(X)=Y\), whence \(u \iff v\). (ii) \(\mathrm{PA}^{+}\) is sound — interpret \(\mathsf c = 0, \mathsf d = 1\) — so \(u \wedge v\) is impossible by Statement 3. (iii) Therefore \(\neg u \wedge \neg v\), and both \(X\) and \(Y\) are true: CUPOD cooperates, DUPOC defects. □

No Löb, no consistency statement, no proof complexity, and no restriction to large \(k\). The Lean development also reports that this argument uses no axioms at all, not even excluded middle: it is constructive.

Why this is not circular. One is tempted to shortcut the whole thing with a “mirror map” sending proofs of \(X\) to proofs of \(Y\), since \(u\) would then produce a proof of a false sentence.

But if \(u\) holds, no such map can exist — so “the map exists” is equivalent to \(\neg u\), not a route to it. Statement 7 escapes because \(\sigma\) is an automorphism of the proof system, defined and verified before \(X\) and \(Y\) are ever mentioned. The map must exist a priori. That distinction is the entire content of the theorem, and it is the one thing we made the Lean development check independently: in a model where \(u\) holds, no length-non-increasing proof-transport exists.

6 What Cannot Work

In the standard arithmetisation, where the actions are encoded as \(0\) and \(1\), \(\sigma\) is not an automorphism — \(\mathrm{PA}\) knows much about \(0\) and \(1\) that is not swap-invariant. Two routes to \(u\) or \(v\) then look available. Both close.

Statement 8 (The canonical certificate is self-defeating). PROVED SCHEMATIC
In any sound formalisation, the bounded-Löb certificate fails for both agents, except on a knife-edge of width \(O(\log k)\).
Proof sketch. The certificate size \(N_X(k)\) is the least solution of \(N \ge \nu\bigl(s(\tilde O(N)+k)\bigr) + O(\log k)\), where \(\nu\) is the cost of proving \(\mathrm{Prf}(\ulcorner\pi\urcorner,\varphi)\) for an explicit \(\pi\). Because (E1) and (E2) are swap-conjugate, the same equation governs \(N_Y(k)\), and the two differ only through the sentence sizes: \(|N_X - N_Y| \le \delta(k) = O(\log k)\). If \(N_X(k) \le k-\delta(k)\), both certificates fit within budget, giving \(u \wedge v\) — impossible. □
Caveat. The size bookkeeping here is asymptotic and is the one argument in this post that we would not defend to the last constant. It is marked SCHEMATIC for that reason. Its corollary — that \(\nu\) and \(s\) cannot both be small, giving \(s(n) \ge n^{1/C}\) for the formalisation overhead exponent \(C\) — is a lower bound of the shape known in the literature, which is mild evidence the bookkeeping is right.

The second route is more dangerous, because it would be cheap. Suppose \(\mathrm{PA}\) could prove the family lower bound uniformly, \(\mathrm{PA}\vdash \forall k\,\neg\Box_kY_k\). A single constant-size proof of a universally quantified statement instantiates at \(k\) for only \(O(\log k)\) symbols, far under budget, and the answer would be \((C,C)\) with none of the consistency expense accounted for above. This route is real in general: there are true \(\psi\) for which \(\neg\Box_k\psi\) is cheaply provable by formalising a proof-complexity lower bound. It is not available here.

Statement 9 (The uniform route is dead). PROVED LEAN-CHECKED
\(\mathrm{PA}\nvdash\forall k\,\neg\Box_kY_k\), and \(\mathrm{PA}\nvdash\forall k\,\neg\Box_kX_k\).
Proof. Suppose \(\mathrm{PA}\vdash_c\forall k\,\neg\Box_kY_k\) for a constant \(c\). Instantiating at the binary numeral \(k\) gives \(\mathrm{PA}\vdash_{c+O(\log k)}X_k\), and Statement 5 then yields \(\mathrm{PA}\vdash_{O(\log k)}\mathrm{Con}_{k-\lambda}\), i.e. \(s(n) = O(\log n)\). This contradicts any superlogarithmic lower bound on \(s\) — in particular the \(s(n) \ge n^{1/C}\) of Statement 8, which is derived here and independent of the literature. □

7 An Equivalence

Read contrapositively, Statement 5 gives more than a barrier. Writing \(a^*(k)\) for the length of the shortest \(\mathrm{PA}\)-proof of \(X_k\):

Statement 10 (Proofs of \(X\) are consistency proofs). PROVED LEAN-CHECKED
\(a^*(k) \ge s(k-\lambda) - O(\log k)\); and when the canonical certificate closes, \(a^*(k) \le \nu\bigl(s(\tilde O(k))\bigr) + \tilde O(k)\). Hence \(a^*(k) = s(k)^{\Theta(1)}\).
Note. The lower half is what the Lean development checks: any in-budget proof of \(X\) has length exceeding \(s - d\). The upper half inherits the SCHEMATIC status of Statement 8.
Statement 11 (The framework does not decide the problem). PROVED LEAN-CHECKED
\((D,C)\) is not a consequence of (E1), (E2) and soundness: there are sound settings satisfying all of them realising each of \((C,C)\), \((D,D)\) and \((D,C)\).
Proof. Three explicit models, given in the Lean file. A proof system with no proofs at all yields \((D,C)\); one whose single proof proves \(X\) yields \((C,C)\); its mirror yields \((D,D)\). □

So the residual case is not a gap in the analysis but a characterisation. DUPOC cooperates with CUPOD if and only if \(\mathrm{PA}\) can certify its own consistency at level \(k\) within \(k\) symbols. Nothing else enters. And the two available techniques provably cannot meet: the collision argument caps at \(s(n) \ge n^{1-o(1)}\), because formalisation overheads are at least the identity, while Statement 5 needs \(s(n) > n\) strictly.

8 Machine Verification

The case analysis above is exactly the sort of thing that is easy to get subtly wrong and impossible to notice, so we formalised it. The development is deliberately abstract: a setting is any proof system with a length measure and soundness, and a game is the pair of sentences with (E1) and (E2). No property of \(\mathrm{PA}\) is assumed anywhere, so the theorems apply to all sound instantiations at once.

structure Setting where
  Sentence : Type
  Prf      : Type
  len      : Prf → Nat
  Proves   : Prf → Sentence → Prop
  Tr       : Sentence → Prop
  sound    : ∀ (p : Prf) (φ : Sentence), Proves p φ → Tr φ

def Setting.Box (S : Setting) (n : Nat) (φ : S.Sentence) : Prop :=
  ∃ p : S.Prf, S.len p ≤ n ∧ S.Proves p φ

structure Game (S : Setting) where
  k  : Nat
  X  : S.Sentence
  Y  : S.Sentence
  E1 : S.Tr Y ↔ ¬ S.Box k X
  E2 : S.Tr X ↔ ¬ S.Box k Y

Eleven theorems check under Lean 4.32.2 against the core library, with no sorry and no custom axioms. The full development is available here — it depends only on core Lean, so lean OpenSourceGT.lean reproduces the audit in a few seconds. Three results of that audit are worth reporting because they were not established by hand beforehand.

First, the Mirror Theorem is constructive: #print axioms reports no dependencies for it, not even excluded middle. Only the trichotomy and the no-exploitation statement use classical logic, and only because they were written with case analysis.

Second, Statement 11 is now formal rather than rhetorical. It is an explicit sound model satisfying every hypothesis in which \((D,C)\) is false. No argument from the modal data alone can settle Open Problem 3, and that is checked rather than asserted.

Third, the anti-circularity point survives contact: from the Mirror Theorem itself the development derives that in the \((C,C)\) model no length-non-increasing proof-transport exists. The swap hypothesis has genuine content and cannot be manufactured after seeing the sentences.

9 What Is Not Verified

Stating this precisely matters more than the results do, because the division of labour between hand argument and machine check is the whole methodological point.

  1. The Ex Falso Reduction (Statement 5) is assumed, not formalised. It enters the Lean development as a hypothesis. Discharging it needs a proof system with Gödel numbering, a \(\mathrm{Prf}\) predicate and length accounting. Bounded provability with proof lengths is not in Mathlib, and to our knowledge not in the existing Lean incompleteness developments either, which work at the unbounded \(\Box\). That is a substantial project on its own.
  2. The existence of \(\sigma\) is assumed, not formalised. The claim that it is an automorphism of \(\mathrm{PA}^{+}\) with \(\sigma(X)=Y\) is a syntactic fact we prove by hand; in Lean it is the swap hypothesis. Verifying it means formalising the language extension, the numbering, and equivariance of axioms and rules.
  3. Statement 8 is asymptotic bookkeeping. It is marked SCHEMATIC and is not Lean-ready; the fixed-point size equation with the \(\nu\) and \(s\) overheads is not a formal statement in our hands.
  4. The literature bound is recalled, not checked. We believe the known window is \(n^{\varepsilon} \le s(n) \le n^{c}\), from Pudlák's work on lengths of finitistic consistency proofs [3]P. Pudlák, “On the length of proofs of finitistic consistency statements in first order theories,” Logic Colloquium '84 (1986). Cited from memory; not re-checked against the paper., and that whether \(s(n) \gtrless n\) is open. We were not able to verify this against the source while writing, so no statement above depends on it: Statement 9 was rewritten to rest on the self-contained bound of Statement 8, since any superlogarithmic lower bound suffices. Readers should treat the citation as background and check it before building on it.

10 Common Objections

  1. “The Mirror Theorem changes the theory, so it does not answer the question.”
    Response
    The framework of Critch et al. is parametric in the theory; the open problem is posed for a sufficiently strong sound theory, and \(\mathrm{PA}^{+}\) is one, conservative over \(\mathrm{PA}\). The agents are unmodified DUPOC and CUPOD. What the theorem shows is that the answer is \((D,C)\) whenever the formalisation does not gratuitously break a symmetry that the agents themselves have. The interesting content is that breaking it is what makes the problem hard.
  2. “Then the answer is encoding-dependent, which is unsatisfying.”
    Response
    Yes, and Statement 11 makes that precise rather than apologising for it. The dependence is exactly \(O(\log k)\) worth of asymmetry introduced by naming the two actions \(0\) and \(1\), and cashing it out is equivalent to separating \(s(n)\) from \(n\). An open problem that turns out to be a known hard problem in disguise has been advanced, not dissolved.
  3. “This is all about Gödelian limits.”
    Response
    It is not, and this is worth stating plainly. \(X_k\) and \(Y_k\) are \(\Delta_0\) sentences; Robinson arithmetic already proves every true one and refutes every false one. Provability and truth coincide here. Every appearance of incompleteness in the problem — the “you can never show no proof exists” intuition — is an artifact of the length bound, not of undecidability.
  4. “One problem, and the interesting case is still open.”
    Response
    Correct. What changed is that the open case is now an equivalence with a named quantity rather than an unmapped question, two of the three routes to it are closed, and the parts that carry the argument are machine-checked. Section 9 says what would have to be built to finish it.

11 Concluding Remarks

Two things seem worth carrying away from this beyond the specific result.

The first is about agent design. The folklore reading of DUPOC and CUPOD is that one is trusting and the other suspicious, and that the surprise is that trust is punished. That reading is wrong. They are one program with one parameter, and an agent's equilibrium behaviour is set by what it demands proof of, not by how generous its default is. For a society of code-reading agents this is the design lesson: the search target is the policy. \((D,C)\) — the outcome in which the proof-seeker takes the doubt-seeker's cooperation without returning it — is the symmetry-fixed point of the construction, robust across formalisations, and not an artifact.

The second is methodological. The part of this work that a reader should trust most is not the part that took the most thought. It is the part a compiler checked in three seconds. The hand arguments in Sections 4 and 6 are where the risk lives, and we have tried to mark them as such rather than let the presence of a Lean file launder the whole document. The verification did not merely confirm what we believed — it told us the Mirror Theorem was constructive, which we had not noticed, and it turned an assertion about independence into a model. That asymmetry, between what one can generate and what one can certify, is the one we have run into every time we have pointed a machine at an open problem. It continues to be the bottleneck, and it continues to be where the useful work is.

References

  1. A. Critch, M. Dennis, S. Russell, “Cooperative and Uncooperative Institution Designs: Surprises and Problems in Open-Source Game Theory,” arXiv:2208.07006 (2022). link
  2. M. Barasz, P. Christiano, B. Fallenstein, M. Herreshoff, P. LaVictoire, E. Yudkowsky, “Robust Cooperation in the Prisoner's Dilemma: Program Equilibrium via Provability Logic,” arXiv:1401.5577 (2014). link
  3. P. Pudlák, “On the length of proofs of finitistic consistency statements in first order theories,” in Logic Colloquium '84, North-Holland (1986), 165–196. Cited from memory; see Section 9, item 4.
  4. M. H. Löb, “Solution of a problem of Leon Henkin,” Journal of Symbolic Logic 20(2) (1955), 115–118.
  5. The Lean 4 theorem prover. github.com/leanprover/lean4

† AER Labs. Correspondence to crystalinecohomology@gmail.com.

@article{kang2026fairbot,
  title  = {FairBot and Its Mirror: An Open Problem in Open-Source Game Theory Is a Proof-Length Problem},
  author = {Kang, Daniel},
  year   = {2026},
  note   = {AER Labs Technical Blog}
}