Proving Your Way to Cooperation: Formalizing Proof-Based Open Source Game Theory in Lean

Open Source Game Theory studies strategic interaction between agents with full mutual transparency, and offers a promising route to robust cooperation in multi-agent systems. Its proof-based branch, in which agents condition on bounded proof search over each other's source code, is theoretically rich, but lacks any mechanized framework, limiting both its empirical study and its integration into practical systems. We address this gap with the first Lean 4 formalization of proof-based Open Source Game Theory, comprising nine open-source programs together with manually written, machine-checked proofs of the outcome theorems that govern their pairwise play. On top of this verified library, we build an agentic pipeline that turns natural-language strategy descriptions into Lean-verified outcome theorems. This pipeline autonomously reproves 40 of the 45 outcome theorems in the resulting bot-pair matrix. As a first application, we use the verified outcomes to enumerate the Nash equilibria of the induced Prisoner’s Dilemma program meta-game and find a broad spectrum of cooperative equilibria absent from the underlying game.